range_eq_top_of_ne_zero — Mathlib

English

If f ∈ Module.Dual K V₁ is nonzero, then the sum of the dimension of its kernel plus one equals the dimension of V₁.

Русский

Пусть f ∈ Module.Dual K V₁ не равно нулю. Тогда сумма размерности ядра f и единицы равна размерности V₁.

LaTeX

$$$\operatorname{finrank}_K(\ker f) + 1 = \operatorname{finrank}_K(V_1)$$$

Lean4

theorem range_eq_top_of_ne_zero {K V₁ : Type*} [Semifield K] [AddCommMonoid V₁] [Module K V₁] {f : Module.Dual K V₁}
    (hf : f ≠ 0) : LinearMap.range f = ⊤ :=
  LinearMap.range_eq_top.mpr (LinearMap.surjective hf)

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