English
Let V and V2 be finite-dimensional vector spaces over a division ring K, and let f: V → V2 be linear. If finrank_K V2 < finrank_K V, then the kernel of f is nontrivial (not equal to {0}).
Русский
Пусть V и V₂ — конечномерные векторные пространства над полем K, и пусть f: V → V₂ линейно. Если dim_K V₂ < dim_K V, то ядро f не тривиально (не равно {0}).
LaTeX
$$$\\operatorname{finrank}_K V_2 < \\operatorname{finrank}_K V \\Rightarrow \\ker f \\neq \\{0\\}$$$
Lean4
theorem ker_ne_bot_of_finrank_lt [FiniteDimensional K V] [FiniteDimensional K V₂] {f : V →ₗ[K] V₂}
(h : finrank K V₂ < finrank K V) : LinearMap.ker f ≠ ⊥ :=
by
have h₁ := f.finrank_range_add_finrank_ker
have h₂ : finrank K (LinearMap.range f) ≤ finrank K V₂ := (LinearMap.range f).finrank_le
suffices 0 < finrank K (LinearMap.ker f) from Submodule.one_le_finrank_iff.mp this
cutsat
