map_sum₂

Mathlib.LinearAlgebra.BilinearMap

URI: https://scilib.ai/kg/mathlib#LinearMap.map_sum₂

← MathLib Explorer

English

For any bilinear map f, f(x1+x2, y) = f(x1,y) + f(x2,y).

Русский

Для билинейного отображения f: f(x1+x2, y) = f(x1,y) + f(x2,y).

LaTeX

$$$ f(x_1 + x_2, y) = f(x_1, y) + f(x_2, y) $$$

Lean4

theorem map_sum₂ {ι : Type*} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (t : Finset ι) (x : ι → M) (y) :
    f (∑ i ∈ t, x i) y = ∑ i ∈ t, f (x i) y :=
  _root_.map_sum (flip f y) _ _

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

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

Разделы

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

Аффилиация

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