index_mul_card — Mathlib

English

Let H be a subgroup of G. Then the product of the index of H in G and the cardinality of H equals the cardinality of G, i.e., [G:H] · |H| = |G|.

Русский

Пусть H — подгруппа G. Тогда произведение индекса H в G на кардинал H равно кардиналу G: [G:H] · |H| = |G|.

LaTeX

$$$[G:H] \cdot |H| = |G|$$$

Lean4

@[to_additive index_mul_card]
theorem index_mul_card : H.index * Nat.card H = Nat.card G := by rw [mul_comm, card_mul_index]

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