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]