linearIndependent_of_sub_mem_range_root'

English

If two root vectors are linearly independent, and their Coxeter weight equals four, then the index set ι is infinite.

Русский

Если два корневых вектора линейно независимы и их кокетерова вес равен четырём, то множество индексов ι бесконечно.

LaTeX

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

Lean4

theorem linearIndependent_of_sub_mem_range_root' [CharZero R] [IsDomain R] [P.IsReduced] {i j : ι}
    (h : P.root i - P.root j ∈ range P.root) : LinearIndependent R ![P.root i, P.root j] :=
  have : IsReflexive R M := .of_isPerfPair P.toLinearMap
  have _i : NoZeroSMulDivisors ℤ M := NoZeroSMulDivisors.int_of_charZero R M
  P.linearIndependent_of_sub_mem_range_root h

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