Mathlib Changelog
v4
Changelog
About
Github
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