polar_comm

Mathlib.LinearAlgebra.QuadraticForm.Basic

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

English

The polar form is symmetric in its two vector arguments: polar f x y = polar f y x.

Русский

Полярная форма симметрична по двум аргументам-вектором: polar f x y = polar f y x.

LaTeX

$$$$ polar f \\; x \\; y = polar f \\; y \\; x. $$$$

Lean4

theorem polar_comm (f : M → N) (x y : M) : polar f x y = polar f y x := by
  rw [polar, polar, add_comm, sub_sub, sub_sub, add_comm (f x) (f y)]

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

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

Разделы

Аффилиация

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