proj — Mathlib

English

The map proj i j is the quadratic map sending x to x_i x_j.

Русский

Квадратичное отображение proj i j отправляет x в x_i x_j.

LaTeX

$$$\mathrm{proj}(i,j) : QuadraticMap R (n \to A) A, \quad (\mathrm{proj}(i,j))(x) = x_i x_j$.$$

Lean4

/-- `proj i j` is the quadratic map sending the vector `x : n → R` to `x i * x j` -/
def proj (i j : n) : QuadraticMap R (n → A) A :=
  linMulLin (@LinearMap.proj _ _ _ (fun _ => A) _ _ i) (@LinearMap.proj _ _ _ (fun _ => A) _ _ j)

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