Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-12-11 04:23
d856bf9b
View on Github →
feat(ring_theory/localization): Clearing denominators (
#10668
)
Estimated changes
Modified
src/ring_theory/localization.lean
added
def
is_localization.common_denom
added
def
is_localization.common_denom_of_finset
added
def
is_localization.finset_integer_multiple
added
theorem
is_localization.finset_integer_multiple_image
added
def
is_localization.integer_multiple
added
theorem
is_localization.map_integer_multiple