OAI/Geometry/Kahler/BaseSphere.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PinchedHartogs.BaseConstruction.sigma line 21
2. instance OAI.PinchedHartogs.BaseConstruction.(instance at line 24) line 24
3. def OAI.PinchedHartogs.BaseConstruction.sphereAction line 31
4. lemma OAI.PinchedHartogs.BaseConstruction.sphereAction_coe line 34
5. def OAI.PinchedHartogs.BaseConstruction.realIsometry line 37
6. lemma OAI.PinchedHartogs.BaseConstruction.sphereAction_preserves line 41
7. lemma OAI.PinchedHartogs.BaseConstruction.sigma_integral_unitary line 72
8. def OAI.PinchedHartogs.BaseConstruction.phaseIsometry line 77
9. lemma OAI.PinchedHartogs.BaseConstruction.phaseIsometry_apply line 81
10. lemma OAI.PinchedHartogs.BaseConstruction.exists_unit_pow_neg_one line 84
11. lemma OAI.PinchedHartogs.BaseConstruction.monomial_sigma_mean line 94
12. lemma OAI.PinchedHartogs.BaseConstruction.sigma_represents line 127