index_prod — Mathlib

English

The index of the direct product of H and K equals the product of their indices: (H × K).index = H.index · K.index.

Русский

Индекс произведения подгрупп равен произведению их индексов: (H × K).index = H.index · K.index.

LaTeX

$$(H \prod K).index = H.index \cdot K.index$$

Lean4

@[to_additive (attr := simp) index_prod]
theorem index_prod (H : Subgroup G) (K : Subgroup G') : (H.prod K).index = H.index * K.index :=
  by
  simp_rw [index, ← Nat.card_prod]
  refine Nat.card_congr ((Quotient.congrRight (fun x y ↦ ?_)).trans (Setoid.prodQuotientEquiv _ _).symm)
  rw [QuotientGroup.leftRel_prod]

Похожие утверждения