reflectionPerm_inv — Mathlib

English

For each i, the reflection i induces a bijection on the set of roots range root.

Русский

Для каждого i отображение отражения порождает биективное отображение на множестве корней range root.

LaTeX

$$$ \text{BijOn}(P.reflection(i), \operatorname{range}(P.root), \operatorname{range}(P.root)) $$$

Lean4

@[simp]
theorem reflectionPerm_inv : (P.reflectionPerm i)⁻¹ = P.reflectionPerm i :=
  (mul_eq_one_iff_eq_inv.mp <| P.reflectionPerm_sq i).symm

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