Registry · Theorem II.T21 established formalized

II.T21 — S^1 as Profinite Limit

S^1 as Profinite Limit

Book II Part 5 Ch. 24

Dependency Graph

Depends on (2)

II.D26 II.T20

Depended on by (1)

II.D27

Lean Formalization

Module: TauLib.BookII.Transcendentals.Circles

Symbol: circle_profinite_check