rank_eq — Mathlib

English

If f: M ≃_R M' is a linear equivalence, then rank_R M = rank_R M'.

Русский

Если существует линейное эквивалентное отображение f: M ≃_R M', тогда ранги пространств совпадают.

LaTeX

$$$\operatorname{Module.rank} R M = \operatorname{Module.rank} R M'$$$

Lean4

/-- Two linearly equivalent vector spaces have the same dimension. -/
theorem rank_eq (f : M ≃ₗ[R] M₁) : Module.rank R M = Module.rank R M₁ :=
  Cardinal.lift_inj.1 f.lift_rank_eq

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