Theorem LocalRing.local_hom_TFAE

Modification history

2024-07-19 18:48

Mathlib/RingTheory/Ideal/LocalRing.lean

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

Modified LocalRing.local_hom_TFAE View on Github →

2023-05-18 11:07

Mathlib/RingTheory/Ideal/LocalRing.lean

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

Added LocalRing.local_hom_TFAE View on Github →