swap_mul_of_ne

Mathlib.LinearAlgebra.Matrix.Swap

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

← MathLib Explorer

English

If a ≠ i and a ≠ j, then (swap R i j * g) a b = g a b for all g.

Русский

Если a ≠ i и a ≠ j, то (swap R i j * g) a b = g a b для всех g.

LaTeX

$$$$ (swap R i j * g) a b = g a b \\\\text{ when } a \\neq i, a \\neq j $$$$

Lean4

theorem swap_mul_of_ne {i j a : n} {b : m} (hai : a ≠ i) (haj : a ≠ j) (g : Matrix n m R) :
    (swap R i j * g) a b = g a b := by simp [swap, PEquiv.toMatrix_toPEquiv_mul, Equiv.swap_apply_of_ne_of_ne hai haj]

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

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

Разделы

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

Аффилиация

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