ortho_comm

Mathlib.LinearAlgebra.SesquilinearForm.Basic

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

English

For a reflexive B, B(x, y) = 0 if and only if B(y, x) = 0.

Русский

Для рефлексивной B: B(x, y) = 0 тогда и только тогда, когда B(y, x) = 0.

LaTeX

$$$\\mathrm{IsRefl}(B) \\Rightarrow (B(x,y)=0 \\iff B(y,x)=0)$$$

Lean4

theorem ortho_comm {x y} : IsOrtho B x y ↔ IsOrtho B y x :=
  ⟨eq_zero H, eq_zero H⟩

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

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

Разделы

Аффилиация

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