pairing_neg_two_neg_two_iff — Mathlib

English

If a pair of roots is linearly independent and a certain Coxeter weight condition holds (weight = 4), the index set ι must be infinite.

Русский

Если пара корней линейно независима и выполняется вес кокетера 4, тогда ι бесконечен.

LaTeX

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

Lean4

/-- See also `RootPairing.pairingIn_neg_two_neg_two_iff`. -/
@[simp]
theorem pairing_neg_two_neg_two_iff : P.pairing i j = -2 ∧ P.pairing j i = -2 ↔ P.root i = -P.root j :=
  by
  simp only [← neg_eq_iff_eq_neg]
  simpa [eq_comm (a := -P.root i), eq_comm (b := j)] using P.pairing_two_two_iff (P.reflectionPerm i i) j

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