of_injective — Mathlib

English

If f: V → W is injective and W is finite-dimensional over K, then V is finite-dimensional over K.

Русский

Если линейное отображение f: V → W инъективно и W конечномерно над K, то V конечномерно над K.

LaTeX

$$IsFiniteDimensional(K, W) ⇒ FiniteDimensional(K, V)$$

Lean4

/-- If the codomain of an injective linear map is finite dimensional, the domain must be as well. -/
theorem of_injective (f : V →ₗ[K] V₂) (w : Function.Injective f) [FiniteDimensional K V₂] : FiniteDimensional K V :=
  Module.Finite.of_injective f w

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