Theorem Polynomial.residueFieldMapCAlgEquiv_symm_X

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_XView 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_XView on Github →