linearIndependent_rows_iff_isUnit

English

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

Русский

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

LaTeX

$$LinearIndependent K A.col ↔ IsUnit A$$

Lean4

theorem linearIndependent_rows_iff_isUnit {A : Matrix m m K} : LinearIndependent K A.row ↔ IsUnit A := by
  rw [← col_transpose, ← mulVec_injective_iff, ← coe_mulVecLin, mulVecLin_transpose, ← vecMul_injective_iff_isUnit,
    coe_vecMulLinear]

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