Theorem OreLocalization.nontrivial_iff

Modification history

2025-08-21 15:31
Mathlib/RingTheory/OreLocalization/Basic.lean
chore(OreLocalization): generalize some results from rings to monoids with zeros (#27174)
Modified OreLocalization.nontrivial_iffView on Github →
2024-06-10 19:57
Mathlib/RingTheory/OreLocalization/Basic.lean
chore(RingTheory/OreLocalization/Basic): Split file and to-additivise (#13559)
Modified OreLocalization.nontrivial_iffView on Github →
2024-06-06 10:40
Mathlib/RingTheory/OreLocalization/Basic.lean
refactor(RingTheory/OreLocalization): Ore localization of modules (#13151) …
Added OreLocalization.nontrivial_iffView on Github →