coxeterWeight_eq_four_iff_not_linearIndependent

English

A variant stating that linear independence for the root pair persists under a reflection-related variant of the root set.

Русский

Вариант устойчивости линейной независимости пары корней под отражательным преобразованием корневых векторов.

LaTeX

$$$$ (P.root i - P.root j) \\in \\operatorname{range}(P.root) \\Rightarrow \\operatorname{LI}_R(\\![P.root i, P.root j]\\!). $$$$

Lean4

/-- See also `RootPairing.coxeterWeightIn_eq_four_iff_not_linearIndependent`. -/
theorem coxeterWeight_eq_four_iff_not_linearIndependent :
    P.coxeterWeight i j = 4 ↔ ¬LinearIndependent R ![P.root i, P.root j] := by
  rw [P.linearIndependent_iff_coxeterWeight_ne_four, not_not]

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