Commit 2025-12-15 10:15 3e3a9f32

View on Github →

feat(RingTheory): residue field of I[X] (#32809)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/FieldTheory/RatFunc/AsPolynomial.lean

added theorem RatFunc.liftRingHom_C

added theorem RatFunc.liftRingHom_X

Modified Mathlib/FieldTheory/RatFunc/Basic.lean

added theorem RatFunc.liftRingHom_algebraMap

added theorem RatFunc.liftRingHom_comp_algebraMap

added theorem RatFunc.liftRingHom_ofFractionRing_algebraMap

Modified Mathlib/RingTheory/Ideal/Quotient/Operations.lean

added def AlgHom.liftOfSurjective

added theorem AlgHom.liftOfSurjective_apply

added theorem AlgHom.liftOfSurjective_comp

added theorem AlgHom.liftOfSurjective_surjective

Created Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean

added def Polynomial.fiberEquivQuotient

added def Polynomial.residueFieldMapCAlgEquiv

added theorem Polynomial.residueFieldMapCAlgEquiv_algebraMap

added theorem Polynomial.residueFieldMapCAlgEquiv_symm_C

added theorem Polynomial.residueFieldMapCAlgEquiv_symm_X