linearIndependent_cols_of_isUnit — Mathlib

English

If A is an invertible square matrix, then its columns are linearly independent.

Русский

Если A — обратимая квадратная матрица, то её столбцы линейно независимы.

LaTeX

$$[Fintype m] {A : Matrix m m R} [DecidableEq m], IsUnit A → LinearIndependent R A.col$$

Lean4

theorem linearIndependent_cols_of_isUnit [Fintype m] {A : Matrix m m R} [DecidableEq m] (ha : IsUnit A) :
    LinearIndependent R A.col := by
  rw [← Matrix.mulVec_injective_iff]
  exact Matrix.mulVec_injective_of_isUnit ha

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