Theorem Polynomial.residueFieldMapCAlgEquiv_symm_C

Modification history

2026-05-01 19:07

Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean

refactor(Localization/AtPrime/Basic): add predicate for algebra instance on `Localization.AtPrime` (#38465) …

Modified Polynomial.residueFieldMapCAlgEquiv_symm_C View on Github →

2025-12-15 10:15

Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean

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

Added Polynomial.residueFieldMapCAlgEquiv_symm_C View on Github →