IsRefl

Mathlib.LinearAlgebra.BilinearForm.Properties

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

English

If B is reflexive, then B x y = 0 implies B y x = 0 for all x,y.

Русский

Если B рефлексивна, то B x y = 0 значит B y x = 0 для любых x,y.

LaTeX

$$H x y → B x y = 0 → B y x = 0$$

Lean4

/-- The proposition that a bilinear form is reflexive -/
def IsRefl (B : BilinForm R M) : Prop :=
  LinearMap.IsRefl B

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

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

Разделы

Аффилиация

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