OAI/Geometry/Cannon/Conformal/Round.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CannonMobius.Round line 14
2. def OAI.CannonMobius.north line 16
3. lemma OAI.CannonMobius.north_norm line 17
4. lemma OAI.CannonMobius.north_ne_zero line 18
5. def OAI.CannonMobius.planeHyperplane line 20
6. def OAI.CannonMobius.roundChart line 25
7. lemma OAI.CannonMobius.roundChart_coe line 29
8. instance OAI.CannonMobius.sphereMetric line 32
9. lemma OAI.CannonMobius.sphere_dist line 35
10. lemma OAI.CannonMobius.roundChart_isometry line 36