ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank

English

Let V and V2 be finite-dimensional with equal finrank. For any linear map f: V → V2, ker f = ⊥ if and only if range f = ⊤.

Русский

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

LaTeX

$$$\operatorname{finrank}_K V = \operatorname{finrank}_K V_2 \Rightarrow (\ker f = \{0\} \iff \operatorname{range} f = V_2)$$$

Lean4

theorem ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank [FiniteDimensional K V] [FiniteDimensional K V₂]
    (H : finrank K V = finrank K V₂) {f : V →ₗ[K] V₂} : LinearMap.ker f = ⊥ ↔ LinearMap.range f = ⊤ := by
  rw [range_eq_top, ker_eq_bot, injective_iff_surjective_of_finrank_eq_finrank H]

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