Registry · Theorem I.T08 established formalized

I.T08 — Categoricity of tau_0

tau_0 is categorical: any two models are uniquely isomorphic. The unique isomorphism maps rho^n(g) to (rho^M)^n(g^M).

Book I Part 2 Ch. 9

Dependency Graph

Depends on (8)

I.T01 I.K1 I.K2 I.K3 I.K4 I.K5 I.K6 I.P01

Lean Formalization

Module: TauLib.BookI.Orbit.Rigidity

Symbol: Tau.Orbit.categoricity