polarSym2

Mathlib.LinearAlgebra.QuadraticForm.Basic

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

Lean4

/-- `QuadraticMap.polar` as a function from `Sym2`. -/
def polarSym2 (f : M → N) : Sym2 M → N :=
  Sym2.lift ⟨polar f, polar_comm _⟩

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

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

Разделы

Аффилиация

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