Theorem IsLocalRing.ResidueField.algebraMap_residue

Modification history

2025-12-02 04:52
Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean
chore(RingTheory/LocalRing): fix problematic instance (#27445) …
Added IsLocalRing.ResidueField.algebraMap_residueView on Github →