add_apply

Mathlib.LinearAlgebra.BilinearForm.Basic

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

English

From B = D it follows that B x y = D x y for all x,y.

Русский

Из B = D следует B(x,y) = D(x,y) для всех x,y.

LaTeX

$$$B = D \Rightarrow \forall x,y:\; B(x,y) = D(x,y)$$$

Lean4

@[simp]
theorem add_apply (x y : M) : (B + D) x y = B x y + D x y :=
  rfl

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

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

Разделы

Аффилиация

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