Theorems · Theorem · group theory
AddMonoidHom.injective_noncommPiCoprod_of_iSupIndep
∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {H : ι → Type u_3} [inst_1 : (i : ι) → AddGroup (H i)]
(ϕ : (i : ι) → H i →+ G) [inst_2 : Fintype ι]
{hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), AddCommute ((ϕ i) x) ((ϕ j) y)},
(iSupIndep fun i => (ϕ i).range) →
(∀ (i : ι), Function.Injective ⇑(ϕ i)) → Function.Injective ⇑(AddMonoidHom.noncommPiCoprod ϕ hcomm)- Defined in
- Mathlib.GroupTheory.NoncommPiCoprod
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites19
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- SetLike.coeproof · cited by 8,199
- Fintypestatement and proof · cited by 7,736
- AddGroupstatement and proof · cited by 4,410
- Finset.univproof · cited by 3,473
- AddSubgroupstatement · cited by 3,232
- AddMonoidHomstatement and proof · cited by 3,230
- map_zeroproof · cited by 1,614
- Pairwisestatement and proof · cited by 516
- Finset.mem_univproof · cited by 361
- AddCommutestatement and proof · cited by 185
- eq_bot_iffproof · cited by 159
Cited by1
Results whose statement or proof uses this declaration.
- AddSubgroup.injective_noncommPiCoprod_of_iSupIndepproof · cited by 0