sub

Mathlib.LinearAlgebra.BilinearForm.Properties

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

← MathLib Explorer

English

Difference of two symmetric bilinear forms is symmetric.

Русский

Разность двух симметричных билинейных форм симметрична.

LaTeX

$$B₁.IsSymm → B₂.IsSymm → (B₁ - B₂).IsSymm$$

Lean4

protected theorem sub {B₁ B₂ : BilinForm R₁ M₁} (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) : (B₁ - B₂).IsSymm :=
  ⟨fun x y => (congr_arg₂ Sub.sub (hB₁.eq x y) (hB₂.eq x y) :)⟩

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

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

Разделы

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

Аффилиация

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