isOrtho_zero_right

Mathlib.LinearAlgebra.BilinearForm.Orthogonal

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

English

If B is reflexive (IsRefl), then orthogonality is symmetric: IsOrtho x y ↔ IsOrtho y x.

Русский

Если B рефлексивна, то ортогональность симметрична: IsOrtho x y ↔ IsOrtho y x.

LaTeX

$$$ B.IsRefl \\Rightarrow (B.IsOrtho x y \\iff B.IsOrtho y x) $$$

Lean4

theorem isOrtho_zero_right (x : M) : IsOrtho B x (0 : M) :=
  zero_right x

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

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

Разделы

Аффилиация

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