linearIndependent_rows_of_isUnit

Mathlib.LinearAlgebra.Matrix.ToLin

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

← MathLib Explorer

English

If A is a unit (invertible) matrix, then its rows are linearly independent.

Русский

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

LaTeX

$$IsUnit A ⇒ LinearIndependent R A.row$$

Lean4

theorem linearIndependent_rows_of_isUnit {A : Matrix m m R} [DecidableEq m] (ha : IsUnit A) :
    LinearIndependent R A.row := by
  rw [← Matrix.vecMul_injective_iff]
  exact Matrix.vecMul_injective_of_isUnit ha

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

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

Разделы

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

Аффилиация

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