Theorem IsLocalRing.of_surjective'

Modification history

2024-12-10 13:44

Mathlib/RingTheory/LocalRing/Basic.lean

refactor(LocalRing/Basic): generalize to non-commutative (semi)rings (#18652) …

Modified IsLocalRing.of_surjective'View on Github →

2024-11-12 11:09

Mathlib/RingTheory/LocalRing/Basic.lean

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

Added IsLocalRing.of_surjective'View on Github →