card_dvd_of_injective — Mathlib

English

If f: α →* H is an injective group homomorphism, then card(α) divides card(H).

Русский

Если f: α →* H инъективно, то card(α) делит card(H).

LaTeX

$$$\operatorname{card}(\alpha) \mid \operatorname{card}(H)$$$

Lean4

@[to_additive]
theorem card_dvd_of_injective (f : α →* H) (hf : Function.Injective f) : Nat.card α ∣ Nat.card H := by
  classical
    calc
    Nat.card α = Nat.card (f.range : Subgroup H) := Nat.card_congr (Equiv.ofInjective f hf)
    _ ∣ Nat.card H := card_subgroup_dvd_card _

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