row_ne_zero

Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

URI: https://scilib.ai/kg/mathlib#Matrix.SpecialLinearGroup.row_ne_zero

← MathLib Explorer

English

For every i, the i-th row of any g ∈ SL(n, R) is not the zero row: g_i ≠ 0.

Русский

Для каждого i-ой строки матрицы g ∈ SL(n,R) она не нулевая: g_i ≠ 0.

LaTeX

$$g_i \neq 0 \quad\text{for all } i$$

Lean4

theorem row_ne_zero [Nontrivial R] (g : SpecialLinearGroup n R) (i : n) : g i ≠ 0 := fun h =>
  g.det_ne_zero <| det_eq_zero_of_row_eq_zero i <| by simp [h]

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

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

Разделы

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

Аффилиация

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