det_transvection_of_ne

Mathlib.LinearAlgebra.Matrix.Transvection

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

← MathLib Explorer

English

For i ≠ j, det(transvection i j c) = 1.

Русский

Для i ≠ j детерминант транспекции равен 1.

LaTeX

$$$$ \\det( \\mathrm{transvection}_{ij}(c) ) = 1 \\quad (i \\neq j). $$$$

Lean4

@[simp]
theorem det_transvection_of_ne (h : i ≠ j) (c : R) : det (transvection i j c) = 1 := by
  rw [← updateRow_eq_transvection i j, det_updateRow_add_smul_self _ h, det_one]

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

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

Разделы

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

Аффилиация

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