OAI/NumberTheory/PiExponent/Geometry/ProjectiveCoordinatePullback.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponentSeshadri.Projective.coordinatePullbackModule line 16
2. def OAI.PiExponentSeshadri.Projective.coordinatePullbackSection line 20
3. def OAI.PiExponentSeshadri.Projective.coordinatePullbackFrame line 23
4. lemma OAI.PiExponentSeshadri.Projective.coordinatePullbackFrame_coefficient line 32
5. def OAI.PiExponentSeshadri.Projective.coordinatePullbackIso line 50
6. def OAI.PiExponentSeshadri.Projective.coordinateLineBundlePullbackIso line 56