Theorems · Definition · group theory
Submonoid.saturation
{M : Type u_1} → [inst : MulOneClass M] → Submonoid M → SaturatedSubmonoid MThe saturation of a submonoid s is the intersection of all saturated submonoids that contain
s.
If M is a commutative monoid, then this is {x : M | ∃ y : M, x * y ∈ s}.
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Quot.sound
- Assumes
- MulOneClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.ofPredproof · cited by 6,101
- Submonoidstatement and proof · cited by 3,086
- MulOneClassstatement and proof · cited by 1,018
- InfSet.sInfproof · cited by 935
- SaturatedSubmonoidstatement and proof · cited by 29
- SaturatedSubmonoid.toSubmonoidproof · cited by 14
Cited by19
Results whose statement or proof uses this declaration.
- Submonoid.gc_saturationstatement and proof · cited by 6
- Submonoid.giSaturationstatement and proof · cited by 3
- Submonoid.le_toSubmonoid_saturationstatement · cited by 2
- Submonoid.saturation_inductionstatement and proof · cited by 1
- Submonoid.saturation_le_iff_lestatement · cited by 1
- SaturatedSubmonoid.bot_defstatement · cited by 0
- SaturatedSubmonoid.iSup_defstatement · cited by 0
- Submonoid.mem_saturation_iffstatement and proof · cited by 0
- Submonoid.mem_saturation_iff'statement · cited by 0
- Submonoid.mem_saturation_iff_exists_dvdstatement and proof · cited by 0
- Submonoid.saturation_botstatement · cited by 0
- Submonoid.saturation_iSupstatement · cited by 0