OAI/NumberTheory/PiExponent/Jets/KoszulTopDifferential.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PiExponentSiegelAux.W31.topDualCoordinateline 12 - theorem
OAI.PiExponentSiegelAux.W31.topDualCoordinate_applyline 16 - def
OAI.PiExponentSiegelAux.W31.scalarConeTopDualCoordinateline 20 - theorem
OAI.PiExponentSiegelAux.W31.scalarConeTopDualCoordinate_applyline 26 - theorem
OAI.PiExponentSiegelAux.W31.scalarConeTopBoundary_evalline 32 - theorem
OAI.PiExponentSiegelAux.W31.scalarConeTopDualCoordinate_boundaryline 45 - theorem
OAI.PiExponentSiegelAux.W31.scalarConeFirstTopBoundary_evalline 57