reflection_sq

Mathlib.LinearAlgebra.RootSystem.Defs

URI: https://scilib.ai/kg/mathlib#RootPairing.reflection_sq

English

The inverse of the i-th reflection permutation is itself.

Русский

Обратная к i-му отражению-перестановке равна самой перестановке.

LaTeX

$$$ (P.reflectionPerm(i))^{-1} = P.reflectionPerm(i) $$$

Lean4

@[simp]
theorem reflection_sq : P.reflection i ^ 2 = 1 :=
  mul_eq_one_iff_eq_inv.mpr rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru