OAI/NumberTheory/PiExponent/Geometry/ProjectiveCoordinateValues.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.PiExponentSeshadri.Projective.evalAway_coordinateline 14 - lemma
OAI.PiExponentSeshadri.Projective.coordinatesMap_pullback_coordinateline 24 - lemma
OAI.PiExponentSeshadri.Projective.sectionFrame_coordinateline 47 - lemma
OAI.PiExponentSeshadri.Frames.normalized_overlap_coefficientsline 71