isSymm_dualProd

Mathlib.LinearAlgebra.QuadraticForm.Dual

URI: https://scilib.ai/kg/mathlib#LinearMap.isSymm_dualProd

English

The quadratic form dualProd is symmetric: the associated bilinear form is symmetric in its two arguments.

Русский

Квадратичная форма dualProd симметрична: связанная билинейная форма симметрична по аргументам.

LaTeX

$$dualProd is symmetric$$

Lean4

theorem isSymm_dualProd : (dualProd R M).IsSymm :=
  ⟨fun _x _y => add_comm _ _⟩

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

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

Разделы

Аффилиация

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