card_dvd_of_surjective — Mathlib

English

For a surjective f: G →* G', Nat.card G' divides Nat.card G.

Русский

Для сюръективного f: G →* G' число Nat.card G' делится на Nat.card G.

LaTeX

$$$ |G'| \mid |G|. $$$

Lean4

@[to_additive]
theorem card_dvd_of_surjective (f : G →* G') (hf : Function.Surjective f) : Nat.card G' ∣ Nat.card G :=
  by
  rw [← Nat.card_congr (QuotientGroup.quotientKerEquivOfSurjective f hf).toEquiv]
  exact Dvd.intro_left (Nat.card f.ker) f.ker.card_mul_index

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