Theorems · Definition · group theory
Submonoid.pi
{ι : Type u_4} →
{M : ι → Type u_5} →
[inst : (i : ι) → MulOneClass (M i)] → Set ι → ((i : ι) → Submonoid (M i)) → Submonoid ((i : ι) → M i)A version of Set.pi for Submonoids. Given an index set I and a family of Submonoids
s : Π i, Submonoid f i, pi I s is the Submonoid of dependent functions f : Π i, f i such
that f i belongs to Pi I s whenever i ∈ I.
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses 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.
- Setstatement and proof · cited by 53,352
- Submonoidstatement and proof · cited by 3,086
- MulOneClassstatement and proof · cited by 1,018
- Set.piproof · cited by 405
- Subsemigroup.carrierproof · cited by 160
- Submonoid.toSubsemigroupproof · cited by 159
Cited by18
Results whose statement or proof uses this declaration.
- Subgroup.piproof · cited by 23
- Submonoid.pi_le_iffstatement and proof · cited by 2
- Submonoid.FG.pistatement and proof · cited by 1
- IsLocalization.iff_map_piEvalRingHomstatement and proof · cited by 1
- Submonoid.iSup_map_mulSinglestatement and proof · cited by 1
- Submonoid.iSup_map_mulSingle_lestatement · cited by 1
- Submonoid.le_comap_mulSingle_pistatement · cited by 1
- Submonoid.mem_pistatement · cited by 0
- Submonoid.closure_pistatement · cited by 0
- Submonoid.IsLocalizationMap.pistatement and proof · cited by 0
- Submonoid.le_pi_iffstatement · cited by 0
- Submonoid.pi_botstatement · cited by 0