Commit 2023-03-14 15:10 05f2f089

View on Github →

feat: port RingTheory.Localization.Integer (#2875)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Localization/Integer.lean

added def IsLocalization.IsInteger

added theorem IsLocalization.exist_integer_multiples

added theorem IsLocalization.exist_integer_multiples_of_finite

added theorem IsLocalization.exist_integer_multiples_of_finset

added theorem IsLocalization.exists_integer_multiple'

added theorem IsLocalization.exists_integer_multiple

added theorem IsLocalization.finsetIntegerMultiple_image

added theorem IsLocalization.isInteger_add

added theorem IsLocalization.isInteger_mul

added theorem IsLocalization.isInteger_one

added theorem IsLocalization.isInteger_smul

added theorem IsLocalization.isInteger_zero

added theorem IsLocalization.map_integerMultiple