OAI/NumberTheory/SiegelZeros/LocalAlgebra/ResidueTensorQuotientAlgEquiv.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.exists_surjective_global_polynomial_quotient_to_local_generic_fiber line 20
2. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.finiteLength_quotient_of_radical_eq_maximalIdeal line 77
3. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.finite_of_finiteLength_of_finite_residue line 104
4. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.length_le_finrank_of_finiteLength_of_finite_residue line 120
5. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.finite_quotient_of_radical_eq_maximalIdeal line 131
6. def OAI.SiegelZeros.WeightedTorusJets.Deformation.residueTensorQuotientAlgEquiv line 147
7. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.finite_residueTensor_of_finite_quotient line 160
8. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.finrank_residueTensor_eq_quotient line 171
9. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.finrank_special_fiber_le_generic line 195
10. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.finrank_special_fiber_le_global_generic line 215
11. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.finite_residueField_mvPolynomial_maximal line 235
12. def OAI.SiegelZeros.WeightedTorusJets.Deformation.polynomialDeformationSpecialFiberAlgEquiv line 250
13. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.finrank_local_quotient_le_pow_of_radical line 282
14. theorem OAI.SiegelZeros.WeightedTorusJets.Deformation.length_local_quotient_le_pow_of_radical line 361