OAI/NumberTheory/PiExponent/Approximation/CoordinateFrameIdentification.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.PiExponentSeshadri.LineBundleFrameCocycle.cocycle_extline 11 - def
OAI.PiExponentSeshadri.LineBundleFrameCocycle.isoOfCoordinateCoefficientsline 18