pairing_neg_one_neg_four_iff' — Mathlib

English

This ties together the linear independence of a root pair with symmetry/reflection relations in RootPairing.

Русский

Это связывает линейную независимость пары корней с симметрией/отражением в RootPairing.

LaTeX

$$$$ \\operatorname{LI}_R(\\![P.root i, P.root j]\\!) \\iff \\text{(root relations under reflections)} $$$$

Lean4

theorem pairing_neg_one_neg_four_iff' (h2 : IsSMulRegular R (2 : R)) :
    P.pairing i j = -1 ∧ P.pairing j i = -4 ↔ P.root j = (-2 : R) • P.root i := by
  simpa [neg_smul, ← neg_eq_iff_eq_neg] using P.pairing_one_four_iff' i (P.reflectionPerm j j) h2

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