Theorems · Theorem · group theory

AddSubgroup.pi_le_iff

∀ {η : Type u_3} {f : η → Type u_4} [inst : (i : η) → AddGroup (f i)] [inst_1 : DecidableEq η] [Finite η]
  {H : (i : η) → AddSubgroup (f i)} {J : AddSubgroup ((i : η) → f i)},
  AddSubgroup.pi Set.univ H ≤ J ↔ ∀ (i : η), AddSubgroup.map (AddMonoidHom.single f i) (H i) ≤ J

For finite index types, the Subgroup.pi is generated by the embeddings of the additive groups.

Defined in

Mathlib.Algebra.Group.Subgroup.Finite

Cited by

2 results in Mathlib

Foundations

Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupDecidableEqFinite