OAI/NumberTheory/SiegelZeros/LocalAlgebra/CoefficientLocalizationMaximal.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.residueAlgHom line 23
2. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.isUnit_aeval_of_residue_independent line 26
3. def OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.rationalCoefficientMap line 36
4. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.rationalCoefficientMap_polynomial line 43
5. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.rationalCoefficientMap_injective line 51
6. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.residue_rationalCoefficientMap_injective line 56
7. abbrev OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.LocalPolynomialRing line 67
8. abbrev OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.LocalPolynomialResidue line 68
9. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.actual_residue_field line 70
10. def OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.residueCoordinate line 73
11. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.localPolynomial_essFiniteType line 76
12. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.localResidue_essFiniteType line 79
13. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.exists_separating_residue_basis line 83
14. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.exists_local_lifts line 91
15. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.residue_coordinate_equations line 99
16. lemma OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.residueCoordinate_aeval line 123
17. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.residueCoordinate_adjoin_top line 133
18. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.exists_coordinate_residue_basis line 146
19. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.exists_coordinate_basis_indices line 160
20. def OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.rationalResidueEquiv line 185
21. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.rationalResidueEquiv_polynomial line 189
22. def OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.residueCoefficientSection line 197
23. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.residueCoefficientSection_residue line 201
24. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.algebraic_field_kernel_isMaximal line 241
25. theorem OAI.SiegelZeros.WeightedTorusJets.PolynomialLocalResidueResolution.extended_kernel_eq line 255