Theorems · Definition · group theory
AddSubgroup.noncommPiCoprod
{G : Type u_1} →
[inst : AddGroup G] →
{ι : Type u_2} →
{H : ι → AddSubgroup G} →
[Fintype ι] → (Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y) → ((i : ι) → ↥(H i)) →+ GThe canonical homomorphism from a family of additive subgroups where elements from different subgroups commute
- Defined in
- Mathlib.GroupTheory.NoncommPiCoprod
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypestatement and proof · cited by 7,736
- AddGroupstatement and proof · cited by 4,410
- AddSubgroupstatement and proof · cited by 3,232
- AddMonoidHomstatement · cited by 3,230
- Pairwisestatement and proof · cited by 516
- AddCommutestatement and proof · cited by 185
- AddSubgroup.subtypeproof · cited by 82
- AddMonoidHom.noncommPiCoprodproof · cited by 8
- AddSubgroup.addCommute_subtype_of_addCommuteproof · cited by 2
Cited by5
Results whose statement or proof uses this declaration.
- AddSubgroup.noncommPiCoprod_singlestatement · cited by 1
- card_dvd_exponent_nsmul_rankproof · cited by 1
- AddSubgroup.injective_noncommPiCoprod_of_iSupIndepstatement · cited by 0
- AddSubgroup.noncommPiCoprod_rangestatement · cited by 0
- AddSubgroup.noncommPiCoprod_applystatement · cited by 0