map_neg₂

Mathlib.LinearAlgebra.BilinearMap

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

English

For any bilinear map f, f(x − y, z) = f(x, z) − f(y, z).

Русский

Для билинейного отображения f выполняется f(x − y, z) = f(x, z) − f(y, z).

LaTeX

$$$ f(x - y, z) = f(x, z) - f(y, z) $$$

Lean4

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

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

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

Разделы

Аффилиация

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