polar_add_left

Mathlib.LinearAlgebra.QuadraticForm.Basic

URI: https://scilib.ai/kg/mathlib#QuadraticMap.polar_add_left

← MathLib Explorer

English

For x, x', y ∈ M, polar Q (x + x') y = polar Q x y + polar Q x' y.

Русский

Для x, x', y ∈ M: polar Q (x+x') y = polar Q x y + polar Q x' y.

LaTeX

$$polar Q (x + x') y = polar Q x y + polar Q x' y$$

Lean4

@[simp]
theorem polar_add_left (x x' y : M) : polar Q (x + x') y = polar Q x y + polar Q x' y :=
  polar_add_left_iff.mpr <| Q.map_add_add_add_map x x' y

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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