associated — Mathlib

English

There is a canonical linear map that sends a quadratic map to its associated symmetric bilinear map.

Русский

Существует каноническое линейное отображение, переводящее квадратичную форму в её ассоциированную симметричную билинейную форму.

LaTeX

$$$\\text{associated} : \\mathrm{QuadraticMap}(R,M,N) \\to \\mathrm{BilinMap}(R,M,N)$ is the linear map sending each quadratic map to its associated symmetric bilinear map.$$

Lean4

/-- `associated` is the linear map that sends a quadratic map over a commutative ring to its
associated symmetric bilinear map. -/
abbrev associated : QuadraticMap R M N →ₗ[R] BilinMap R M N :=
  associatedHom R

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