map_zero₂

Mathlib.LinearAlgebra.BilinearMap

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

English

For any bilinear map f, f(-x, y) = - f(x, y) for all x, y.

Русский

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

LaTeX

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

Lean4

theorem map_zero₂ (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (y) : f 0 y = 0 :=
  (flip f y).map_zero

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

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

Разделы

Аффилиация

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