Commit 2025-08-21 15:31 4f17c83b

View on Github →

chore(OreLocalization): generalize some results from rings to monoids with zeros (#27174)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/OreLocalization/Basic.lean

added theorem OreLocalization.nontrivial_iff

added theorem OreLocalization.subsingleton_iff

Created Mathlib/RingTheory/OreLocalization/NonZeroDivisors.lean

added theorem OreLocalization.nontrivial_of_nonZeroDivisors

added theorem OreLocalization.nontrivial_of_nonZeroDivisorsLeft

added theorem OreLocalization.nontrivial_of_nonZeroDivisorsRight

Modified Mathlib/RingTheory/OreLocalization/Ring.lean

deleted theorem OreLocalization.nontrivial_iff

deleted theorem OreLocalization.nontrivial_of_nonZeroDivisors

deleted theorem OreLocalization.nontrivial_of_nonZeroDivisorsLeft

deleted theorem OreLocalization.nontrivial_of_nonZeroDivisorsRight

deleted theorem OreLocalization.subsingleton_iff