OAI/NumberTheory/PiExponent/Polynomials/PolynomialLocalResidueResolution.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentJets.PolynomialLocalResidueResolution.residueAlgHom line 15
  2. theorem OAI.PiExponentJets.PolynomialLocalResidueResolution.isUnit_aeval_of_residue_independent line 18
  3. def OAI.PiExponentJets.PolynomialLocalResidueResolution.rationalCoefficientMap line 28
  4. theorem OAI.PiExponentJets.PolynomialLocalResidueResolution.rationalCoefficientMap_polynomial line 35
  5. theorem OAI.PiExponentJets.PolynomialLocalResidueResolution.rationalCoefficientMap_injective line 43
  6. theorem OAI.PiExponentJets.PolynomialLocalResidueResolution.residue_rationalCoefficientMap_injective line 48
  7. abbrev OAI.PiExponentJets.PolynomialLocalResidueResolution.LocalPolynomialRing line 58
  8. abbrev OAI.PiExponentJets.PolynomialLocalResidueResolution.LocalPolynomialResidue line 59
  9. theorem OAI.PiExponentJets.PolynomialLocalResidueResolution.actual_residue_field line 61
  10. def OAI.PiExponentJets.PolynomialLocalResidueResolution.residueCoordinate line 64
  11. theorem OAI.PiExponentJets.PolynomialLocalResidueResolution.localPolynomial_essFiniteType line 67
  12. theorem OAI.PiExponentJets.PolynomialLocalResidueResolution.localResidue_essFiniteType line 70
  13. theorem OAI.PiExponentJets.PolynomialLocalResidueResolution.exists_separating_residue_basis line 74
  14. theorem OAI.PiExponentJets.PolynomialLocalResidueResolution.exists_local_lifts line 82
  15. theorem OAI.PiExponentJets.PolynomialLocalResidueResolution.residue_coordinate_equations line 90