QuadraticForm — Mathlib

English

A quadratic form on a module is a quadratic map Q: M → R, i.e., a map equipped with a notion of polarity giving rise to a bilinear form.

Русский

Квадратичная форма на модуле есть отображение Q: M → R, являющееся квадратичным отображением, порождающим билинейную форму через поляризацию.

LaTeX

$$$$ \\text{QuadraticForm}(R,M) \\;:=\\; \\text{QuadraticMap} \\; R \\; M \\; R. $$$$

Lean4

/-- A quadratic form on a module. -/
abbrev QuadraticForm : Type _ :=
  QuadraticMap R M R

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