isSymm_def

Mathlib.LinearAlgebra.BilinearForm.Properties

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

English

A bilinear form B is symmetric if and only if -B is symmetric.

Русский

Билинейная форма B симметрична если и только если -B симметрична.

LaTeX

$$(-B).IsSymm \iff B.IsSymm$$

Lean4

theorem isSymm_def : IsSymm B ↔ ∀ x y, B x y = B y x
    where
  mp := fun ⟨h⟩ ↦ h
  mpr h := ⟨h⟩

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

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

Разделы

Аффилиация

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