coxeterWeight_nonneg — Mathlib

English

The Weyl group of a root pairing is the closure of the set of reflections of the Equiv.reflection P, forming a subgroup of Aut P.

Русский

Группа Вейля пары корней есть замыкание множества отражений Equiv.reflection P, образующее подгруппу Aut P.

LaTeX

$$$ P.weylGroup = \\operatorname{closure} (\\operatorname{range}(\\Equiv.reflection P)) $$$

Lean4

theorem coxeterWeight_nonneg [IsStrictOrderedRing S] : 0 ≤ P.coxeterWeightIn S i j :=
  by
  dsimp [coxeterWeightIn]
  rcases lt_or_ge 0 (P.pairingIn S i j) with h | h
  · exact le_of_lt <| mul_pos h ((zero_lt_pairingIn_iff B i j).mp h)
  · have hn : P.pairingIn S j i ≤ 0 := by rwa [← not_lt, ← zero_lt_pairingIn_iff B i j, not_lt]
    exact mul_nonneg_of_nonpos_of_nonpos h hn

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