Theorem IsLocalRing.not_isLocalRing_tfae

Modification history

2025-04-15 09:16

Mathlib/RingTheory/LocalRing/NonLocalRing.lean

feat(RingTheory/LocalRing): results for non-local rings (#24043)

Added IsLocalRing.not_isLocalRing_tfae View on Github →