mulVec_injective_of_invertible — Mathlib

English

Let A be an invertible square matrix over a field K. Then the linear map x ↦ A x is injective (i.e., its kernel is {0}).

Русский

Пусть A — обратимая квадратная матрица над полем K. Тогда линейное отображение x ↦ A x инъективно (ядеро равно {0}).

LaTeX

$$$\text{If } A \in M_m(K) \text{ is invertible, then the linear map } x \mapsto A x \text{ is injective, i.e. } \ker(A) = \{0\}. $$$

Lean4

theorem mulVec_injective_of_invertible (A : Matrix m m K) [Invertible A] : Function.Injective A.mulVec :=
  mulVec_injective_iff_isUnit.2 <| isUnit_of_invertible A

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