Theorems · Inductive type · group theory
SaturatedSubmonoid
(M : Type u_1) → [MulOneClass M] → Type u_1
A saturated submonoid is a submonoid s that satisfies x * y ∈ s → x ∈ s ∧ y ∈ s.
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- MulOneClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MulOneClassstatement · cited by 1,018
Cited by38
Results whose statement or proof uses this declaration.
- Submonoid.saturationstatement and proof · cited by 18
- SaturatedSubmonoid.toSubmonoidstatement and proof · cited by 14
- Submonoid.gc_saturationstatement and proof · cited by 6
- Submonoid.giSaturationstatement · cited by 3
- SaturatedSubmonoid.mem_sInfstatement and proof · cited by 2
- SaturatedSubmonoid.mulSaturatedstatement and proof · cited by 2
- SaturatedSubmonoid.extstatement and proof · cited by 1
- SaturatedSubmonoid.toSubmonoid_injectivestatement and proof · cited by 1
- Submonoid.saturation_inductionstatement and proof · cited by 1
- Submonoid.saturation_le_iff_lestatement and proof · cited by 1
- SaturatedSubmonoid.mk.injstatement · cited by 1
- SaturatedSubmonoid.mk.noConfusionstatement · cited by 1