coxeterWeight_zero_iff_isOrthogonal

English

If NeZero 2 and IsDomain hold, coxeterWeight i j = 0 if and only if IsOrthogonal i j.

Русский

При условиях NeZero 2 и IsDomain, coxeterWeight i j = 0 если и только если IsOrthogonal i j.

LaTeX

$$$$ \\mathrm{coxeterWeight}(i,j) = 0 \\iff \\mathrm{IsOrthogonal}(i,j). $$$$

Lean4

theorem coxeterWeight_zero_iff_isOrthogonal [NeZero (2 : R)] [IsDomain R] :
    P.coxeterWeight i j = 0 ↔ P.IsOrthogonal i j :=
  by
  have : IsReflexive R M := .of_isPerfPair P.toLinearMap
  simp [coxeterWeight, IsOrthogonal, P.pairing_eq_zero_iff (i := i) (j := j)]

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