transvection_zero

Mathlib.LinearAlgebra.Matrix.Transvection

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

English

For any i, j, transvection i j 0 equals the identity.

Русский

Для любых i, j транспекция i j 0 равна единице.

LaTeX

$$$$ \\mathrm{transvection}_{ij}(0) = I. $$$$

Lean4

@[simp]
theorem transvection_zero : transvection i j (0 : R) = 1 := by simp [transvection]

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

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

Разделы

Аффилиация

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