finrank_map_eq — Mathlib

English

Pushforwards of finite-dimensional submodules along a linear equivalence preserve finrank.

Русский

Образы подмодулей под линейным эквивалентом сохраняют конечную размерность.

LaTeX

$$$\\operatorname{finrank}_R (p.map (f : M \\to N)) = \\operatorname{finrank}_R p$$$

Lean4

/-- Pushforwards of finite-dimensional submodules along a `LinearEquiv` have the same finrank. -/
theorem finrank_map_eq (f : M ≃ₗ[R] N) (p : Submodule R M) : finrank R (p.map (f : M →ₗ[R] N)) = finrank R p :=
  (f.submoduleMap p).finrank_eq.symm

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