OAI/NumberTheory/Jacobsthal/Siegel/ResidueTensorQuotientAlgEquiv.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.WeightedTorusJets.Deformation.exists_surjective_global_polynomial_quotient_to_local_generic_fiber line 23
2. theorem OAI.Erdos970.WeightedTorusJets.Deformation.finiteLength_quotient_of_radical_eq_maximalIdeal line 81
3. theorem OAI.Erdos970.WeightedTorusJets.Deformation.finite_of_finiteLength_of_finite_residue line 108
4. theorem OAI.Erdos970.WeightedTorusJets.Deformation.length_le_finrank_of_finiteLength_of_finite_residue line 124
5. theorem OAI.Erdos970.WeightedTorusJets.Deformation.finite_quotient_of_radical_eq_maximalIdeal line 135
6. def OAI.Erdos970.WeightedTorusJets.Deformation.residueTensorQuotientAlgEquiv line 152
7. theorem OAI.Erdos970.WeightedTorusJets.Deformation.finite_residueTensor_of_finite_quotient line 165
8. theorem OAI.Erdos970.WeightedTorusJets.Deformation.finrank_residueTensor_eq_quotient line 176
9. theorem OAI.Erdos970.WeightedTorusJets.Deformation.finrank_special_fiber_le_generic line 200
10. theorem OAI.Erdos970.WeightedTorusJets.Deformation.finrank_special_fiber_le_global_generic line 220
11. theorem OAI.Erdos970.WeightedTorusJets.Deformation.finite_residueField_mvPolynomial_maximal line 241
12. def OAI.Erdos970.WeightedTorusJets.Deformation.polynomialDeformationSpecialFiberAlgEquiv line 260
13. theorem OAI.Erdos970.WeightedTorusJets.Deformation.finrank_local_quotient_le_pow_of_radical line 294
14. theorem OAI.Erdos970.WeightedTorusJets.Deformation.length_local_quotient_le_pow_of_radical line 373