isRefl

Mathlib.LinearAlgebra.SesquilinearForm.Basic

URI: https://scilib.ai/kg/mathlib#LinearMap.IsSymm.isRefl

English

A bilinear form B is symmetric if and only if B equals its flip: B = B.flip.

Русский

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

LaTeX

$$$B.IsSymm \\iff B = B.flip$$$

Lean4

theorem isRefl (H : B.IsSymm) : B.IsRefl := fun x y H1 ↦
  by
  rw [← H.eq]
  simp [H1]

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

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

Разделы

Аффилиация

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