map_sub₂

Mathlib.LinearAlgebra.BilinearMap

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

English

For any bilinear map f, f(x, y1 + y2) = f(x, y1) + f(x, y2).

Русский

Для билинейного отображения f: f(x, y1 + y2) = f(x, y1) + f(x, y2).

LaTeX

$$$ f(x, y_1 + y_2) = f(x, y_1) + f(x, y_2) $$$

Lean4

theorem map_sub₂ (f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P') (x y z) : f (x - y) z = f x z - f y z :=
  (flip f z).map_sub _ _

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

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

Разделы

Аффилиация

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