map_smul

Mathlib.LinearAlgebra.QuadraticForm.Basic

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

English

For every scalar a ∈ R and every x ∈ M, the value of the quadratic map scales by a^2, i.e., Q(a · x) = (a · a) · Q(x).

Русский

Для каждого скаляра a ∈ R и каждого x ∈ M выполняется Q(a · x) = a^2 · Q(x).

LaTeX

$$Q(a x) = a^2 \cdot Q(x)$$

Lean4

protected theorem map_smul (a : R) (x : M) : Q (a • x) = (a * a) • Q x :=
  Q.toFun_smul a x

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

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

Разделы

Аффилиация

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