English
For a family of subgroups H(i) indexed by a finite set i, the index of the product subgroup equals the product of the indices: (Subgroup.pi Set.univ H).index = ∏ i (H(i).index).
Русский
Для семейства подгрупп H(i) индекс произведной подгруппы равен произведению индексов: (Subgroup.pi Set.univ H).index = ∏ i (H(i).index).
LaTeX
$$(Subgroup.pi Set.univ H).index = ∏ i, (H i).index$$
Lean4
@[to_additive (attr := simp)]
theorem index_pi {ι : Type*} [Fintype ι] (H : ι → Subgroup G) : (Subgroup.pi Set.univ H).index = ∏ i, (H i).index :=
by
simp_rw [index, ← Nat.card_pi]
refine Nat.card_congr ((Quotient.congrRight (fun x y ↦ ?_)).trans (Setoid.piQuotientEquiv _).symm)
rw [QuotientGroup.leftRel_pi]
