sq

Mathlib.LinearAlgebra.QuadraticForm.Basic

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

English

The map sq is the quadratic map sending x to x^2 in an algebra.

Русский

Квадратичное отображение sq отправляет вектор x в x^2 в алгебре.

LaTeX

$$$\mathrm{sq} : QuadraticMap R A A \quad\text{defined by}\quad \mathrm{sq}(x) = x\cdot x.$$$

Lean4

/-- `sq` is the quadratic map sending the vector `x : A` to `x * x` -/
@[simps!]
def sq : QuadraticMap R A A :=
  linMulLin LinearMap.id LinearMap.id

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

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

Разделы

Аффилиация

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