eq_zero

Mathlib.LinearAlgebra.BilinearForm.Properties

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

English

The negation of a reflexive bilinear form is reflexive.

Русский

Негирование рефлексивной билинейной формы сохраняет свойство рефлексивности.

LaTeX

$$(-B).IsRefl$$

Lean4

theorem eq_zero (H : B.IsRefl) : ∀ {x y : M}, B x y = 0 → B y x = 0 := fun {x y} => H x y

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

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

Разделы

Аффилиация

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