rank_linearMap — Mathlib

English

The rank of the space of linear maps equals the product of ranks of M and N, after lifting to the appropriate base.

Русский

Ранг пространства линейных отображений равен произведению рангов M и N после соответствующего подъема базовых рангов.

LaTeX

$$$$ \mathrm{rank}_S(\mathrm{Hom}_R(M, N)) = \mathrm{lift}(\mathrm{rank}_R M) \cdot \mathrm{lift}(\mathrm{rank}_S N). $$$$

Lean4

theorem rank_linearMap : Module.rank S (M →ₗ[R] N) = lift.{w} (Module.rank R M) * lift.{v} (Module.rank S N) := by
  rw [(linearMapEquivFun R S M N).rank_eq, rank_fun_eq_lift_mul, ← finrank_eq_card_chooseBasisIndex, ←
    finrank_eq_rank R, lift_natCast]

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