Theorem IsLocalRing.not_isLocalRing_def

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_def View on Github →