IsOrthogonal — Mathlib

English

Two roots i and j are orthogonal when both pairings vanish: pairing i j = 0 and pairing j i = 0.

Русский

Два корня i и j ортогональны тогда и только тогда, когда обе паруются нулевые: pairing i j = 0 и pairing j i = 0.

LaTeX

$$$$ \\text{IsOrthogonal}(P,i,j) \\;\\equiv\\; \\bigl( P.pairing(i,j)=0 \\bigr) \\wedge \\bigl( P.pairing(j,i)=0 \\bigr). $$$$

Lean4

/-- Two roots are orthogonal when they are fixed by each others' reflections. -/
def IsOrthogonal : Prop :=
  pairing P i j = 0 ∧ pairing P j i = 0

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