instSubtypeMemSubmoduleMapLinearMapId

English

Pushforwards of finite-dimensional submodules under a linear map are finite-dimensional.

Русский

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

LaTeX

$$FiniteDimensional K (p.map f)$$

Lean4

/-- Pushforwards of finite-dimensional submodules are finite-dimensional. -/
instance (f : V →ₗ[K] V₂) (p : Submodule K V) [FiniteDimensional K p] : FiniteDimensional K (p.map f) :=
  Module.Finite.map _ _

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