mul_transvection_apply_same

Mathlib.LinearAlgebra.Matrix.Transvection

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

← MathLib Explorer

English

T_{ij}(c) = I + c E_{ij}.

Русский

T_{ij}(c) = I + c E_{ij}.

LaTeX

$$$$ \\mathrm{transvection}_{ij}(c) = I + c\, E_{ij}. $$$$

Lean4

@[simp]
theorem mul_transvection_apply_same (a : n) (c : R) (M : Matrix n n R) :
    (M * transvection i j c) a j = M a j + c * M a i := by simp [transvection, Matrix.mul_add, mul_comm]

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

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

Разделы

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

Аффилиация

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