isUnit_iff_range_eq_top — Mathlib

English

A linear map is a unit iff its range is the entire space.

Русский

Линейное отображение является единицей тогда и только тогда, когда его образ равен всему пространству.

LaTeX

$$$[\operatorname{FiniteDimensional}_K V] (f: V \to V): \operatorname{IsUnit} f \iff \operatorname{range} f = \ top$$$

Lean4

theorem isUnit_iff_range_eq_top [FiniteDimensional K V] (f : V →ₗ[K] V) : IsUnit f ↔ (LinearMap.range f) = ⊤ := by
  rw [isUnit_iff_ker_eq_bot, ker_eq_bot_iff_range_eq_top]

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