finrank_linearMap — Mathlib

English

The rank of the space of linear maps from M to S over R equals the rank of M over R.

Русский

Ранг пространства линейных отображений M → S равен рангу M над R.

LaTeX

$$$$ \mathrm{rank}_S(\mathrm{Hom}_R(M, S)) = \mathrm{rank}_R M. $$$$

Lean4

/-- The `finrank` of `M →ₗ[R] N` as an `S`-module is `(finrank R M) * (finrank S N)`. -/
theorem finrank_linearMap : finrank S (M →ₗ[R] N) = finrank R M * finrank S N := by
  simp_rw [finrank, rank_linearMap, toNat_mul, toNat_lift]

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