Theorems · Definition · group theory
AddSubmonoid.pi
{ι : Type u_4} →
{M : ι → Type u_5} →
[inst : (i : ι) → AddZeroClass (M i)] → Set ι → ((i : ι) → AddSubmonoid (M i)) → AddSubmonoid ((i : ι) → M i)A version of Set.pi for AddSubmonoids. Given an index set I and a family
of AddSubmonoids s : Π i, AddSubmonoid f i, pi I s is the AddSubmonoid of dependent
functions f : Π i, f i such that f i belongs to pi I s whenever i ∈ I.
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses Quot.sound
- Assumes
- AddZeroClass
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
- AddZeroClassstatement and proof · cited by 1,237
- AddSubmonoidstatement and proof · cited by 1,178
- Set.piproof · cited by 405
- AddSubmonoid.toAddSubsemigroupproof · cited by 198
- AddSubsemigroup.carrierproof · cited by 198
Cited by21
Results whose statement or proof uses this declaration.
- AddSubgroup.piproof · cited by 26
- AddSubmonoid.mem_pistatement · cited by 3
- DFinsupp.mker_mapRangeAddMonoidHomstatement · cited by 3
- DFinsupp.mrange_mapRangeAddMonoidHomstatement and proof · cited by 3
- AddSubmonoid.pi_le_iffstatement and proof · cited by 2
- AddSubmonoid.single_mem_pistatement and proof · cited by 2
- AddSubmonoid.iSup_map_singlestatement and proof · cited by 1
- AddSubmonoid.iSup_map_single_lestatement · cited by 1
- AddSubmonoid.FG.pistatement and proof · cited by 1
- AddSubmonoid.le_comap_single_pistatement · cited by 1
- AddSubmonoid.pi_botstatement · cited by 0
- AddSubmonoid.pi_emptystatement · cited by 0