OAI/NumberTheory/SiegelZeros/LocalAlgebra/GradedIdealQuotient.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SiegelZeros.WeightedTorusJets.Geometry.gradedIdealQuotient line 14
2. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.finrank_homogeneousSubmodule_fin line 34
3. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.linear_quotient_map_homogeneous_mem line 45
4. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.linear_quotient_map_gradedSMul line 63
5. theorem OAI.SiegelZeros.WeightedTorusJets.normalization_quotient_finite_torsionFree_finiteVariables line 97
6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.hilbertPolynomial_normalization_finiteVariables line 135
7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.projectiveDegree_eq_normalization_rank_finiteVariables line 184