coxeterWeightIn_ne_four — Mathlib

English

If RootPairing is valued in a subring, the LI of the root pair corresponds to a nonzero weight in the valued Coxeter data.

Русский

Если RootPairing ценится в подкольце, линейная независимость пары корней соответствует ненулевому весу в кокетерских данных.

LaTeX

$$$$ \\text{LI in } R \\iff P.coxeterWeightIn S i j \\neq 4. $$$$

Lean4

theorem coxeterWeightIn_ne_four [P.IsReduced] (h : i ≠ j) (h' : P.root i ≠ -P.root j) : P.coxeterWeightIn S i j ≠ 4 :=
  by
  rw [ne_eq, coxeterWeightIn_eq_four_iff_not_linearIndependent, not_not]
  exact IsReduced.linearIndependent P h h'

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