OAI/NumberTheory/PiExponent/Polynomials/PolynomialCoefficientLocalization.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponentSiegelAux.W09.SplitPolynomial line 12
  2. abbrev OAI.PiExponentSiegelAux.W09.CoefficientPolynomial line 13
  3. abbrev OAI.PiExponentSiegelAux.W09.CoefficientFractionField line 14
  4. abbrev OAI.PiExponentSiegelAux.W09.FractionCoefficientPolynomial line 15
  5. def OAI.PiExponentSiegelAux.W09.coefficientDenominators line 17
  6. abbrev OAI.PiExponentSiegelAux.W09.PolynomialCoefficientLocalization line 21
  7. theorem OAI.PiExponentSiegelAux.W09.coefficientRename_injective line 23
  8. theorem OAI.PiExponentSiegelAux.W09.mem_coefficientDenominators line 28
  9. theorem OAI.PiExponentSiegelAux.W09.sumAlgEquiv_coefficientRename line 33
  10. theorem OAI.PiExponentSiegelAux.W09.sumAlgEquiv_coefficientDenominators line 39
  11. def OAI.PiExponentSiegelAux.W09.polynomialCoefficientLocalizationEquiv line 65
  12. theorem OAI.PiExponentSiegelAux.W09.polynomialCoefficientLocalizationEquiv_algebraMap line 71
  13. theorem OAI.PiExponentSiegelAux.W09.polynomialCoefficientLocalizationEquiv_X_inl line 80
  14. theorem OAI.PiExponentSiegelAux.W09.polynomialCoefficientLocalizationEquiv_X_inr line 87
  15. theorem OAI.PiExponentSiegelAux.W09.polynomialCoefficientLocalizationEquiv_coefficient line 96
  16. theorem OAI.PiExponentSiegelAux.W09.polynomialCoefficientLocalizationEquiv_mk' line 105
  17. theorem OAI.PiExponentSiegelAux.W09.coefficientDenominator_isUnit line 116