English
Let α be a group and S a subgroup. For any subset t ⊆ α, the size of the product t · S equals the product of the size of S and the size of the image of t in the quotient α / S; i.e. card(t · S) = card(S) · card(t.image(↑) : Set(α / S)).
Русский
Пусть α — группа, S — подпгруппа. Для любого подмножества t ⊆ α размер произведения t · S равен произведению размера S на размер образа t в фактор-группе α / S; то есть card(t · S) = card(S) · card(t.image(↑) : Set(α / S)).
LaTeX
$$$\operatorname{card}(t * s) = \operatorname{card}(s) \cdot \operatorname{card}\bigl( t.\mathrm{image}(\uparrow) : \mathrm{Set}(\alpha / s) \bigr).$$$
Lean4
@[to_additive]
theorem card_mul_eq_card_subgroup_mul_card_quotient (s : Subgroup α) (t : Set α) :
Nat.card (t * s : Set α) = Nat.card s * Nat.card (t.image (↑) : Set (α ⧸ s)) :=
by
rw [← Nat.card_prod, Nat.card_congr]
apply Equiv.trans _ (QuotientGroup.preimageMkEquivSubgroupProdSet _ _)
rw [QuotientGroup.preimage_image_mk]
convert Equiv.refl ↑(t * s)
aesop (add simp [Set.mem_mul])
