isUnit_iff_ker_eq_bot — Mathlib

English

A linear map is a unit iff its kernel is zero.

Русский

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

LaTeX

$$$[\operatorname{FiniteDimensional}_K V] \text{(f)}: \operatorname{IsUnit} f \iff \ker f = \{0\}$$$

Lean4

theorem isUnit_iff_ker_eq_bot [FiniteDimensional K V] (f : V →ₗ[K] V) : IsUnit f ↔ (LinearMap.ker f) = ⊥ :=
  by
  constructor
  · rintro ⟨u, rfl⟩
    exact LinearMap.ker_eq_bot_of_inverse u.inv_mul
  · intro h_inj
    rw [ker_eq_bot] at h_inj
    exact
      ⟨⟨f, (LinearEquiv.ofInjectiveEndo f h_inj).symm.toLinearMap, LinearEquiv.ofInjectiveEndo_right_inv f h_inj,
          LinearEquiv.ofInjectiveEndo_left_inv f h_inj⟩,
        rfl⟩

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