ker_eq_bot_iff_range_eq_top — Mathlib

English

For a finite-dimensional endomorphism f: V → V, ker f = {0} iff range f = V.

Русский

Для конечномерного отображения f: V→V верно: ядро равно нулю тогда и только тогда образ равен всему пространству.

LaTeX

$$$\ker f = \{0\} \iff \operatorname{range} f = V$$$

Lean4

theorem ker_eq_bot_iff_range_eq_top [FiniteDimensional K V] {f : V →ₗ[K] V} :
    LinearMap.ker f = ⊥ ↔ LinearMap.range f = ⊤ := by rw [range_eq_top, ker_eq_bot, injective_iff_surjective]

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