OAI/Geometry/Kahler/BasePhaseReal.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.PinchedHartogs.BaseConstruction.phaseSum_conjline 20 - lemma
OAI.PinchedHartogs.BaseConstruction.phaseSum_real_bandline 29 - lemma
OAI.PinchedHartogs.BaseConstruction.phaseSum_integralline 52