simple — Mathlib

English

For a fixed index i, the simple reflection s_i in W is defined via the Coxeter system and represents a generating reflection corresponding to i.

Русский

Для фиксированного индекса i простое отражение s_i в W задаётся через систему Коксетера и представляет порождающее отражение, соответствующее i.

LaTeX

$$$s_i \in W, \quad s_i = \text{image of } i \text{ under the reflection map}$$$

Lean4

/-- The simple reflection of `W` at the index `i`. -/
def simple (i : B) : W :=
  cs.mulEquiv.symm (PresentedGroup.of i)

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