Theorems · Theorem · group theory

Subgroup.pi_le_iff

∀ {η : Type u_3} {f : η → Type u_4} [inst : (i : η) → Group (f i)] [inst_1 : DecidableEq η] [Finite η]
  {H : (i : η) → Subgroup (f i)} {J : Subgroup ((i : η) → f i)},
  Subgroup.pi Set.univ H ≤ J ↔ ∀ (i : η), Subgroup.map (MonoidHom.mulSingle f i) (H i) ≤ J

For finite index types, the Subgroup.pi is generated by the embeddings of the 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

GroupDecidableEqFinite