Commit 2025-04-15 09:16 96081764

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/LocalRing/NonLocalRing.lean

added theorem IsLocalRing.exists_surjective_of_not_isLocalRing.{u}

added theorem IsLocalRing.not_isLocalRing_def

added theorem IsLocalRing.not_isLocalRing_of_nontrivial_pi

added theorem IsLocalRing.not_isLocalRing_of_prod_of_nontrivial

added theorem IsLocalRing.not_isLocalRing_tfae