polar_neg

Mathlib.LinearAlgebra.QuadraticForm.Basic

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

English

The polar form is linear with respect to negation: polar(-f) x y = -polar(f) x y.

Русский

Полярная форма линейна по отрицанию: polar(-f) x y = -polar(f) x y.

LaTeX

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

Lean4

theorem polar_neg (f : M → N) (x y : M) : polar (-f) x y = -polar f x y := by
  simp only [polar, Pi.neg_apply, sub_eq_add_neg, neg_add]

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

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

Разделы

Аффилиация

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