ofIdx_smul — Mathlib

English

Let P be a RootPairing. For every i in ι and every m in M, the Weyl group element corresponding to i acts on m by the i-th reflection.

Русский

Пусть P - корневая пара. Для каждого i из ι и каждого m в M элемент Weyl-группы, соответствующий i, действует на m как i‑й отражение.

LaTeX

$$$ w_i \\cdot m = s_i(m) \\quad\\text{for all } i\\in\\iota, m\\in M,$ where $w_i$ denotes the Weyl-group element given by $i$ and $s_i$ the i-th root reflection.$$

Lean4

@[simp]
theorem ofIdx_smul (i : ι) (m : M) : weylGroup.ofIdx P i • m = Equiv.reflection P i • m :=
  rfl

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