neg_eq

Mathlib.LinearAlgebra.BilinearForm.Properties

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

English

For an alternating bilinear form B1 and any x, y, one has -B1(x,y) = B1(y,x).

Русский

Для чередующей билинейной формы B1 и любых x, y имеет место -B1(x,y) = B1(y,x).

LaTeX

$$$-B(x,y) = B(y,x)$ for all x,y$$

Lean4

theorem neg_eq (H : B₁.IsAlt) (x y : M₁) : -B₁ x y = B₁ y x :=
  LinearMap.IsAlt.neg H x y

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

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

Разделы

Аффилиация

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