OAI/NumberTheory/SiegelZeros/LocalAlgebra/PolynomialCoefficientLocalization.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SiegelZeros.SiegelZerosAwei.W09.SplitPolynomial line 14
2. abbrev OAI.SiegelZeros.SiegelZerosAwei.W09.CoefficientPolynomial line 15
3. abbrev OAI.SiegelZeros.SiegelZerosAwei.W09.CoefficientFractionField line 16
4. abbrev OAI.SiegelZeros.SiegelZerosAwei.W09.FractionCoefficientPolynomial line 17
5. def OAI.SiegelZeros.SiegelZerosAwei.W09.coefficientDenominators line 19
6. abbrev OAI.SiegelZeros.SiegelZerosAwei.W09.PolynomialCoefficientLocalization line 23
7. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.coefficientRename_injective line 25
8. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.mem_coefficientDenominators line 30
9. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.sumAlgEquiv_coefficientRename line 35
10. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.sumAlgEquiv_coefficientDenominators line 41
11. def OAI.SiegelZeros.SiegelZerosAwei.W09.polynomialCoefficientLocalizationEquiv line 67
12. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.polynomialCoefficientLocalizationEquiv_algebraMap line 73
13. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.polynomialCoefficientLocalizationEquiv_X_inl line 82
14. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.polynomialCoefficientLocalizationEquiv_X_inr line 89
15. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.polynomialCoefficientLocalizationEquiv_coefficient line 98
16. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.polynomialCoefficientLocalizationEquiv_mk' line 107
17. theorem OAI.SiegelZeros.SiegelZerosAwei.W09.coefficientDenominator_isUnit line 118