toMatrix'_smul

Mathlib.LinearAlgebra.QuadraticForm.Basic

URI: https://scilib.ai/kg/mathlib#QuadraticMap.toMatrix'_smul

← MathLib Explorer

English

The matrix of a quadratic form is symmetric.

Русский

Матрица квадратичной формы симметрична.

LaTeX

$$Q.toMatrix' IsSymm$$

Lean4

theorem toMatrix'_smul (a : R) (Q : QuadraticMap R (n → R) R) : (a • Q).toMatrix' = a • Q.toMatrix' := by
  simp only [toMatrix', LinearEquiv.map_smul, LinearMap.map_smul]

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

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

Разделы

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

Аффилиация

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