English
If G and M are finite groups and f: G → M satisfies |ker f| ≤ |G|/|M|, then f is surjective.
Русский
Если G и M конечны и f: G → M удовлетворяет |ker f| ≤ |G|/|M|, то f сюръективен.
LaTeX
$$Nat.card f.ker ≤ Nat.card G / Nat.card M → Function.Surjective f$$
Lean4
@[to_additive AddMonoidHom.surjective_of_card_ker_le_div]
theorem surjective_of_card_ker_le_div {G M : Type*} [Group G] [Group M] [Finite G] [Finite M] (f : G →* M)
(h : Nat.card f.ker ≤ Nat.card G / Nat.card M) : Function.Surjective f :=
by
refine range_eq_top.1 <| SetLike.ext' <| Set.eq_of_subset_of_ncard_le (Set.subset_univ _) ?_
rw [Subgroup.coe_top, Set.ncard_univ, ← Nat.card_coe_set_eq, SetLike.coe_sort_coe, ←
Nat.card_congr (QuotientGroup.quotientKerEquivRange f).toEquiv]
exact Nat.le_of_mul_le_mul_left (f.ker.card_mul_index ▸ Nat.mul_le_of_le_div _ _ _ h) Nat.card_pos
