lift_rank_map_eq — Mathlib

English

For a linear equivalence f and submodule p, the lifted rank of p.map f equals the lifted rank of p.

Русский

Для линейного эквивалента f и подмодуля p ранг образа p через f равен подъему ранга p.

LaTeX

$$$\mathrm{lift} \big( \operatorname{Module.rank} R (p.map (f : M \to M')) \big) = \mathrm{lift} \big( \operatorname{Module.rank} R p \big)$$$

Lean4

theorem lift_rank_map_eq (f : M ≃ₗ[R] M') (p : Submodule R M) :
    lift.{v} (Module.rank R (p.map (f : M →ₗ[R] M'))) = lift.{v'} (Module.rank R p) :=
  (f.submoduleMap p).lift_rank_eq.symm

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