map_add_self

Mathlib.LinearAlgebra.QuadraticForm.Basic

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

← MathLib Explorer

English

For all x ∈ M, Q(x + x) = 4 · Q(x).

Русский

Для любого x ∈ M выполняется Q(x+x) = 4 · Q(x).

LaTeX

$$Q(x+x) = 4 \cdot Q(x)$$

Lean4

theorem map_add_self (x : M) : Q (x + x) = 4 • Q x :=
  by
  rw [← two_smul R x, Q.map_smul, ← Nat.cast_smul_eq_nsmul R]
  norm_num
    -- not @[simp] because it is superseded by `ZeroHomClass.map_zero`

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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