ker_toLin_eq_bot — Mathlib

English

If a matrix A has nonzero determinant, the kernel of the endomorphism toLin(b,b,A) is trivial (i.e., only {0}).

Русский

Если det(A) ≠ 0, то ядро эндоморфизма toLin(b,b,A) тривиально.

LaTeX

$$$\\ker(\\operatorname{toLin}(b,b,A)) = \\{0\\}$, \\text{whenever } \\det A \\neq 0$$$

Lean4

theorem ker_toLin_eq_bot [DecidableEq n] (A : Matrix n n R) (hA : IsUnit A.det) : LinearMap.ker (toLin b b A) = ⊥ :=
  ker_eq_bot.mpr (toLinearEquiv b A hA).injective

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