invFun_smul

Mathlib.RingTheory.MatrixAlgebra

URI: https://scilib.ai/kg/mathlib#MatrixEquivTensor.invFun_smul

English

invFun respects scalar multiplication: invFun(a · M) = (a ⊗ 1) · invFun(M)

Русский

invFun сохраняет скалярное умножение: invFun(a · M) = (a ⊗ 1) · invFun(M)

LaTeX

$$$ invFun(n,R,A)(a \cdot M) = (a \otimes 1) * invFun(n,R,A)(M) $$$

Lean4

@[simp]
theorem invFun_smul (a : A) (M : Matrix n n A) : invFun n R A (a • M) = a ⊗ₜ 1 * invFun n R A M := by
  simp [invFun, Finset.mul_sum]

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

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

Разделы

Аффилиация

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