Theorem IsLocalRing.not_isLocalRing_of_nontrivial_pi

Modification history

2025-04-28 14:19
Mathlib/RingTheory/LocalRing/NonLocalRing.lean
chore(*): fix some Fintype/Finite assumptions (#24424) …
Modified IsLocalRing.not_isLocalRing_of_nontrivial_piView on Github →
2025-04-15 09:16
Mathlib/RingTheory/LocalRing/NonLocalRing.lean
feat(RingTheory/LocalRing): results for non-local rings (#24043)
Added IsLocalRing.not_isLocalRing_of_nontrivial_piView on Github →