sub_apply

Mathlib.LinearAlgebra.BilinearForm.Basic

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

English

The difference of bilinear forms distributes: (B - D) x y = B x y - D x y.

Русский

Разность билинейных форм распределяется: (B - D) x y = B x y - D x y.

LaTeX

$$$$(B - D) x y = B x y - D x y$$$$

Lean4

@[simp]
theorem sub_apply (x y : M₁) : (B₁ - D₁) x y = B₁ x y - D₁ x y :=
  rfl

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

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

Разделы

Аффилиация

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