Theorem IsLocalRing.exists_surjective_of_not_isLocalRing.{u}

Modification history

2025-04-15 09:16
Mathlib/RingTheory/LocalRing/NonLocalRing.lean
feat(RingTheory/LocalRing): results for non-local rings (#24043)
Added IsLocalRing.exists_surjective_of_not_isLocalRing.{u}View on Github →