OAI/NumberTheory/PiExponent/Geometry/ProjectiveCoordinateChartMap.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PiExponentSeshadri.Projective.coordinateChartMapline 15 - lemma
OAI.PiExponentSeshadri.Projective.coordinateChartMap_factorline 20 - lemma
OAI.PiExponentSeshadri.Projective.coordinateChartMap_ratioline 26