OAI/NumberTheory/PiExponent/LocalAlgebra/IteratedKoszulExactness.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PiExponentSiegelAux.W30.scalarCone_positive_exactline 10 - theorem
OAI.PiExponentSiegelAux.W30.iterateScalarCones_exactline 31 - theorem
OAI.PiExponentSiegelAux.W30.regularSequenceComplex_exactline 77