linearIndependent_iff_coxeterWeightIn_ne_four

English

A standard equivalence: the LI criterion with weight not equal to four is equivalent to a non-identity reflection relation under algebra maps.

Русский

Стандартная эквивалентность: критерий LI при весе, не равном четырём, эквивалентен неидентичному отражательному отношению под отображениями алгебра.

LaTeX

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

Lean4

theorem linearIndependent_iff_coxeterWeightIn_ne_four :
    LinearIndependent R ![P.root i, P.root j] ↔ P.coxeterWeightIn S i j ≠ 4 := by
  rw [linearIndependent_iff_coxeterWeight_ne_four, ← P.algebraMap_coxeterWeightIn S, ← map_ofNat (algebraMap S R),
    (algebraMap_injective S R).ne_iff]

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