OAI/NumberTheory/SiegelZeros/Structure/KoszulTopTerm.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SiegelZeros.SiegelZerosAwei.W31.scalarConeTopEquivline 16 - def
OAI.SiegelZeros.SiegelZerosAwei.W31.iterateScalarConesTopEquivline 24 - def
OAI.SiegelZeros.SiegelZerosAwei.W31.regularSequenceTopEquivline 40 - def
OAI.SiegelZeros.SiegelZerosAwei.W31.regularSequenceTopDualEquivline 48 - theorem
OAI.SiegelZeros.SiegelZerosAwei.W31.regularSequenceTopDualEquiv_applyline 52