Theorem IsLocalRing.not_isLocalRing_of_prod_of_nontrivial

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_of_prod_of_nontrivialView on Github →