OAI/NumberTheory/SiegelZeros/Hilbert/HomogeneousSections.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SiegelZeros.WeightedTorusJets.W64.finite_exponents_of_degreeline 18 - instance
OAI.SiegelZeros.WeightedTorusJets.W64.homogeneousSection_finiteline 22 - theorem
OAI.SiegelZeros.WeightedTorusJets.W64.homogeneousSection_finrankline 31 - def
OAI.SiegelZeros.WeightedTorusJets.W64.homogeneousMultiplyline 44 - theorem
OAI.SiegelZeros.WeightedTorusJets.W64.homogeneousMultiply_injectiveline 53 - theorem
OAI.SiegelZeros.WeightedTorusJets.W64.homogeneousCokernel_finrank_addline 60