polarBilin — Mathlib

English

Define polarBilin as the bilinear map associated to Q, given by polar, polar_add_left, polar_smul_left, polar_add_right, polar_smul_right.

Русский

Определяем polarBilin как билинейную карту, ассоциированную с Q, заданную поляризацией и связанными свойствами.

LaTeX

$${R M N} ⟶ BilinMap R M N$$

Lean4

/-- `QuadraticMap.polar` as a bilinear map -/
@[simps!]
def polarBilin : BilinMap R M N :=
  LinearMap.mk₂ R (polar Q) (polar_add_left Q) (polar_smul_left Q) (polar_add_right Q) (polar_smul_right Q)

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