coxeterWeight_ne_four_of_linearIndependent

English

From linear independence of a pair of roots, the Coxeter weight cannot be four.

Русский

Линейная независимость пары корней исключает кокетер вес равный четырём.

LaTeX

$$$$ \\operatorname{LI}_R(\\![P.root i, P.root j]\\!) \\Rightarrow P.coxeterWeight i j \\neq 4. $$$$

Lean4

theorem coxeterWeight_ne_four_of_linearIndependent [NeZero (2 : R)] [NoZeroSMulDivisors ℤ M]
    (hl : LinearIndependent R ![P.root i, P.root j]) : P.coxeterWeight i j ≠ 4 :=
  by
  intro contra
  have := P.infinite_of_linearIndependent_coxeterWeight_four hl contra
  exact not_finite ι

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