Def LocalRing.ResidueField.map

Modification history

2024-07-19 18:48

Mathlib/RingTheory/Ideal/LocalRing.lean

chore: Split and move RingTheory.Ideal.LocalRing (#14829) …

Modified LocalRing.ResidueField.map View on Github →

2023-05-18 11:07

Mathlib/RingTheory/Ideal/LocalRing.lean

feat: port RingTheory.Ideal.LocalRing (#4066)

Added LocalRing.ResidueField.map View on Github →