inv_simple — Mathlib

English

Inverse of a simple reflection s_i equals itself: (s_i)^{-1} = s_i, since s_i is its own inverse in the Coxeter group.

Русский

Обратное к простому отражению s_i равно самому отражению: (s_i)^{-1} = s_i, поскольку оно есть собственное обратное в группе Коксетера.

LaTeX

$$$s_i^{-1} = s_i$$$

Lean4

@[simp]
theorem inv_simple (i : B) : (s i)⁻¹ = s i :=
  (eq_inv_of_mul_eq_one_right (cs.simple_mul_simple_self i)).symm

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