OAI/NumberTheory/PiExponent/Polynomials/PolynomialPrimeClosedPointEquiv.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponentJets.PolynomialLocalResidueResolution.coefficientClosedPoint line 14
2. instance OAI.PiExponentJets.PolynomialLocalResidueResolution.coefficientClosedPoint_isMaximal line 19
3. abbrev OAI.PiExponentJets.PolynomialLocalResidueResolution.CoefficientClosedLocal line 27
4. theorem OAI.PiExponentJets.PolynomialLocalResidueResolution.closedLocal_isLocalizationAtOriginal line 29
5. def OAI.PiExponentJets.PolynomialLocalResidueResolution.originalLocalCoefficientLocalEquiv line 48
6. def OAI.PiExponentJets.PolynomialLocalResidueResolution.closedPolynomialIdeal line 54
7. instance OAI.PiExponentJets.PolynomialLocalResidueResolution.closedPolynomialIdeal_isMaximal line 58
8. def OAI.PiExponentJets.PolynomialLocalResidueResolution.polynomialPrimeClosedPointEquiv line 64
9. def OAI.PiExponentJets.PolynomialLocalResidueResolution.polynomialPrimeClosedPointResidueEquiv line 72