OAI/Geometry/Kahler/BasePotentialControl.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.PinchedHartogs.BaseConstruction.base_matrix_value_boundline 20 - lemma
OAI.PinchedHartogs.BaseConstruction.norm_jet_add_mulline 37 - lemma
OAI.PinchedHartogs.BaseConstruction.basePotential_chart_controlline 44