Commit 2026-03-03 16:35 18978c4c

View on Github →

feat(Algebra): saturation of a submonoid (#31132) This PR defines the saturation of a submonoid and the type of saturated submonoids. It is used for the context of localisations. Caveat: there is a similarly named predicate called AddSubgroup.Saturated. Zulip:

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Group/Submonoid/Saturation.lean

added structure SaturatedAddSubmonoid

added theorem SaturatedSubmonoid.bot_def

added theorem SaturatedSubmonoid.ext'

added theorem SaturatedSubmonoid.ext

added theorem SaturatedSubmonoid.iSup_def

added theorem SaturatedSubmonoid.mem_bot_iff

added theorem SaturatedSubmonoid.mem_sInf

added theorem SaturatedSubmonoid.mem_toSubmonoid

added theorem SaturatedSubmonoid.mem_top

added theorem SaturatedSubmonoid.sSup_def

added theorem SaturatedSubmonoid.sup_def

added theorem SaturatedSubmonoid.toSubmonoid_injective

added structure SaturatedSubmonoid

added theorem Submonoid.MulSaturated.iInf

added theorem Submonoid.MulSaturated.inf

added theorem Submonoid.MulSaturated.mul_mem_iff

added theorem Submonoid.MulSaturated.of_left

added theorem Submonoid.MulSaturated.of_right

added theorem Submonoid.MulSaturated.sInf

added theorem Submonoid.MulSaturated.top

added def Submonoid.MulSaturated

added theorem Submonoid.gc_saturation

added def Submonoid.giSaturation

added theorem Submonoid.le_toSubmonoid_saturation

added theorem Submonoid.mem_saturation_iff'

added theorem Submonoid.mem_saturation_iff

added theorem Submonoid.mem_saturation_iff_exists_dvd

added def Submonoid.saturation

added theorem Submonoid.saturation_bot

added theorem Submonoid.saturation_iSup

added theorem Submonoid.saturation_induction

added theorem Submonoid.saturation_le_iff_le

added theorem Submonoid.saturation_sSup

added theorem Submonoid.saturation_sup

added theorem Submonoid.saturation_toSubmonoid

added theorem Submonoid.saturation_top

Modified Mathlib/GroupTheory/Subgroup/Saturated.lean

deleted theorem AddSubgroup.ker_saturated

added theorem AddSubmonoid.ker_saturated

deleted def Subgroup.Saturated

deleted theorem Subgroup.saturated_iff_npow

added def Submonoid.PowSaturated

added theorem Submonoid.powSaturated_iff_npow