mulVec_injective_iff_isUnit — Mathlib

English

Linear independence of the rows of A over K is equivalent to A being a unit.

Русский

Линейная независимость строк матрицы A над полем K эквивалентна тому, что A — единица.

LaTeX

$$LinearIndependent K A.row ↔ IsUnit A$$

Lean4

theorem mulVec_injective_iff_isUnit {A : Matrix m m K} : Function.Injective A.mulVec ↔ IsUnit A :=
  by
  rw [← isUnit_transpose, ← vecMul_injective_iff_isUnit]
  simp_rw [vecMul_transpose]

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