lift_rank_range_of_injective — Mathlib

English

If f is injective, the rank of the range of f equals the rank of the domain M, up to universe lifting.

Русский

Если f инъективно отображает M в M', то ранг образа f равен рангу M (с подъёмом вселенных).

LaTeX

$$$\operatorname{lift} \big( \operatorname{Module.rank} R (\operatorname{range} f) \big) = \operatorname{lift} \big( \operatorname{Module.rank} R M \big)$$$

Lean4

theorem lift_rank_range_of_injective (f : M →ₗ[R] M') (h : Injective f) :
    lift.{v} (Module.rank R (LinearMap.range f)) = lift.{v'} (Module.rank R M) :=
  (LinearEquiv.ofInjective f h).lift_rank_eq.symm

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