dfinsuppFamily_add

Mathlib.LinearAlgebra.Multilinear.DFinsupp

URI: https://scilib.ai/kg/mathlib#MultilinearMap.dfinsuppFamily_add

← MathLib Explorer

English

The dfinsuppFamily map of the zero family is identically zero.

Русский

dfinsuppFamily от нулевойFamily равна нулю.

LaTeX

$$$\dfinsuppFamily 0 = 0$$$

Lean4

@[simp]
theorem dfinsuppFamily_add (f g : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) (N p)) :
    dfinsuppFamily (f + g) = dfinsuppFamily f + dfinsuppFamily g := by ext; simp

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

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

Разделы

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

Аффилиация

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