OAI/Geometry/Kahler/BasePhaseMoments.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.PinchedHartogs.BaseConstruction.real_cast_eq_conjline 20 - lemma
OAI.PinchedHartogs.BaseConstruction.phase_real_momentline 23 - lemma
OAI.PinchedHartogs.BaseConstruction.phase_real_sum_momentline 44