isRefl

Mathlib.LinearAlgebra.BilinearForm.Properties

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

English

A bilinear form B is symmetric precisely when B(x,y) = B(y,x) for all x,y.

Русский

Билинейная форма B симметрична тогда и только тогда, когда для всех x,y выполняется B(x,y) = B(y,x).

LaTeX

$$IsSymm B \iff ∀ x y, B x y = B y x$$

Lean4

theorem isRefl (H : B.IsSymm) : B.IsRefl := fun x y H1 => H.eq x y ▸ H1

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

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

Разделы

Аффилиация

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