isRefl_neg

Mathlib.LinearAlgebra.BilinearForm.Properties

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem isRefl_neg {B : BilinForm R₁ M₁} : (-B).IsRefl ↔ B.IsRefl :=
  ⟨fun h => neg_neg B ▸ h.neg, IsRefl.neg⟩

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

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

Разделы

Аффилиация

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