smul

Mathlib.LinearAlgebra.BilinearForm.Properties

URI: https://scilib.ai/kg/mathlib#LinearMap.BilinForm.IsSymm.smul

← MathLib Explorer

English

If B is symmetric, then for any a, a•B is symmetric.

Русский

Если B симметрична, то для любого a симметрична и a•B.

LaTeX

$$$B.IsSymm \Rightarrow (a \cdot B).IsSymm$$$

Lean4

protected theorem smul {α} [Monoid α] [DistribMulAction α R] [SMulCommClass R α R] (a : α) {B : BilinForm R M}
    (hB : B.IsSymm) : (a • B).IsSymm :=
  ⟨fun x y => congr_arg (a • ·) (hB.eq x y)⟩

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

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

Разделы

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

Аффилиация

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