isOrtho_def

Mathlib.LinearAlgebra.SesquilinearForm.Basic

URI: https://scilib.ai/kg/mathlib#LinearMap.isOrtho_def

English

Two elements are orthogonal if their pairing under a sesquilinear map is zero.

Русский

Два элемента ортогональны относительно билинеарной карты, если их скалярное произведение равно нулю.

LaTeX

$$$IsOrtho(B)(x,y) \iff B(x,y) = 0$$$

Lean4

theorem isOrtho_def {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} {x y} : B.IsOrtho x y ↔ B x y = 0 :=
  Iff.rfl

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

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

Разделы

Аффилиация

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