linearIndependent_cols_of_det_ne_zero

Mathlib.LinearAlgebra.Matrix.Determinant.Basic

URI: https://scilib.ai/kg/mathlib#Matrix.linearIndependent_cols_of_det_ne_zero

← MathLib Explorer

English

If det A ≠ 0, then the columns of A are linearly independent.

Русский

Если det A ≠ 0, то столбцы A линейно независимы.

LaTeX

$$A.det \\\\neq 0 \\\\Rightarrow \\\\text{LinearIndependent}_R (A.col)$$

Lean4

theorem linearIndependent_cols_of_det_ne_zero [IsDomain R] {A : Matrix m m R} (hA : A.det ≠ 0) :
    LinearIndependent R A.col :=
  Matrix.linearIndependent_rows_of_det_ne_zero (by simpa [Matrix.col])

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru