rank_le_of_surjective — Mathlib

English

Let f: G →* H be surjective. Then rank(H) ≤ rank(G).

Русский

Пусть f : G →* H сюръективен. Тогда rank(H) ≤ rank(G).

LaTeX

$$$\text{If } f: G \to H \text{ is surjective, then } \operatorname{rank}(H) \le \operatorname{rank}(G).$$$

Lean4

@[to_additive]
theorem rank_le_of_surjective [FG G] [FG H] (f : G →* H) (hf : Surjective f) : rank H ≤ rank G := by
  classical
  obtain ⟨S, hS1, hS2⟩ := rank_spec G
  trans (S.image f).card
  · apply rank_le
    rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]
  · exact Finset.card_image_le.trans_eq hS1

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