finrank_eq — Mathlib

English

If f : M ≃ₗ[R] N is a linear isomorphism, then finrank_R M = finrank_R N.

Русский

Если существует линейное эквивалентное отображение f: M ≃ₗ[R] N, то finrank_R M = finrank_R N.

LaTeX

$$$\\operatorname{finrank}_R M = \\operatorname{finrank}_R N$$$

Lean4

/-- The dimension of a finite-dimensional space is preserved under linear equivalence. -/
theorem finrank_eq (f : M ≃ₗ[R] N) : finrank R M = finrank R N :=
  by
  unfold finrank
  rw [← Cardinal.toNat_lift, f.lift_rank_eq, Cardinal.toNat_lift]

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