add_right

Mathlib.LinearAlgebra.BilinearForm.Basic

URI: https://scilib.ai/kg/mathlib#LinearMap.BilinForm.add_right

English

For any z, B(x, y+z) = B(x, y) + B(x, z).

Русский

Для любого z, B(x, y+z) = B(x, y) + B(x, z).

LaTeX

$$$\forall x,y,z:\; B(x, y+z) = B(x,y) + B(x,z)$$$

Lean4

theorem add_right (x y z : M) : B x (y + z) = B x y + B x z :=
  map_add _ _ _

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

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

Разделы

Аффилиация

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