rank_congr — Mathlib

English

Rank is preserved under isomorphisms: if e: G ≃* H is a group isomorphism, then rank(G) = rank(H).

Русский

Ранг сохраняется при изоморфизмах: если e: G ≃* H — изоморфизм групп, то rank(G) = rank(H).

LaTeX

$$$\operatorname{rank}(G) = \operatorname{rank}(H) \quad\text{if } G \cong H.$$$

Lean4

@[to_additive]
theorem rank_congr [FG G] [FG H] (e : G ≃* H) : rank G = rank H :=
  le_antisymm (rank_le_of_surjective e.symm e.symm.surjective) (rank_le_of_surjective e e.surjective)

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