rank_range_le — Mathlib

English

For FG G and any homomorphism f : G →* H, rank of the image of f is at most rank(G).

Русский

Для FG группы G и любого гомоморфизма f : G →* H ранг образа f не больше ранга G.

LaTeX

$$$\operatorname{rank}(\operatorname{range}(f)) \le \operatorname{rank}(G).$$$

Lean4

@[to_additive]
theorem rank_range_le [FG G] {f : G →* H} : rank f.range ≤ rank G :=
  rank_le_of_surjective f.rangeRestrict f.rangeRestrict_surjective

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