Commit 2024-06-10 19:57 936ffbfa

View on Github →

chore(RingTheory/OreLocalization/Basic): Split file and to-additivise (#13559)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/MonoidLocalization.lean

Modified Mathlib/RingTheory/OreLocalization/Basic.lean

deleted theorem OreLocalization.nontrivial_iff

deleted theorem OreLocalization.nontrivial_of_nonZeroDivisors

deleted theorem OreLocalization.numeratorHom_inj

deleted theorem OreLocalization.right_distrib

deleted theorem OreLocalization.subsingleton_iff

deleted def OreLocalization.universalHom

deleted theorem OreLocalization.universalHom_apply

deleted theorem OreLocalization.universalHom_commutes

deleted theorem OreLocalization.universalHom_unique

Modified Mathlib/RingTheory/OreLocalization/OreSet.lean

Created Mathlib/RingTheory/OreLocalization/Ring.lean

added theorem OreLocalization.nontrivial_iff

added theorem OreLocalization.nontrivial_of_nonZeroDivisors

added theorem OreLocalization.numeratorHom_inj

added theorem OreLocalization.right_distrib

added theorem OreLocalization.subsingleton_iff

added def OreLocalization.universalHom

added theorem OreLocalization.universalHom_apply

added theorem OreLocalization.universalHom_commutes

added theorem OreLocalization.universalHom_unique