Def LocalRing.residue

Modification history

2024-11-12 11:09

Mathlib/RingTheory/LocalRing/ResidueField/Defs.lean

chore: rename `LocalRing` to `IsLocalRing` (#18774)

Deleted LocalRing.residue View on Github →

2024-07-19 18:48

Mathlib/RingTheory/Ideal/LocalRing.lean

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

Modified LocalRing.residue View on Github →

2023-05-18 11:07

Mathlib/RingTheory/Ideal/LocalRing.lean

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

Added LocalRing.residue View on Github →