card_comap_dvd_of_injective — Mathlib

English

Let K be a subgroup of H and f: α →* H an injective homomorphism. Then card(K.comap f) divides card(K).

Русский

Пусть K — подгруппа H и f: α →* H инъективно. Тогда card(K.comap f) делит card(K).

LaTeX

$$$\operatorname{card}(K.comap f) \mid \operatorname{card}(K)$$$

Lean4

@[to_additive]
theorem card_comap_dvd_of_injective (K : Subgroup H) (f : α →* H) (hf : Function.Injective f) :
    Nat.card (K.comap f) ∣ Nat.card K :=
  calc
    Nat.card (K.comap f) = Nat.card ((K.comap f).map f) := Nat.card_congr (equivMapOfInjective _ _ hf).toEquiv
    _ ∣ Nat.card K := card_dvd_of_le (map_comap_le _ _)

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