Commit 2023-05-03 13:39 b2959acb

View on Github →

feat: port RingTheory.Localization.InvSubmonoid (#3384)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Localization/InvSubmonoid.lean

added theorem IsLocalization.finiteType_of_monoid_fg

added def IsLocalization.invSubmonoid

added theorem IsLocalization.mem_invSubmonoid_iff_exists_mk'

added theorem IsLocalization.mul_toInvSubmonoid

added theorem IsLocalization.smul_toInvSubmonoid

added theorem IsLocalization.span_invSubmonoid

added theorem IsLocalization.submonoid_map_le_is_unit

added theorem IsLocalization.surj''

added theorem IsLocalization.toInvSubmonoid_eq_mk'

added theorem IsLocalization.toInvSubmonoid_mul

added theorem IsLocalization.toInvSubmonoid_surjective