invFun_add

Mathlib.RingTheory.MatrixAlgebra

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

← MathLib Explorer

English

invFun is additive with respect to matrix addition

Русский

invFun является аддитивным по отношению к сложению матриц

LaTeX

$$$ invFun(n,R,A)(M+N) = invFun(n,R,A)(M) + invFun(n,R,A)(N) $$$

Lean4

@[simp]
theorem invFun_add (M N : Matrix n n A) : invFun n R A (M + N) = invFun n R A M + invFun n R A N := by
  simp [invFun, add_tmul, Finset.sum_add_distrib]

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

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

Разделы

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

Аффилиация

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