isReflection_simple

Mathlib.GroupTheory.Coxeter.Inversion

URI: https://scilib.ai/kg/mathlib#CoxeterSystem.isReflection_simple

English

If t is a reflection, then its inverse t^{-1} is also a reflection.

Русский

Если t — отражение, то и его обратное t^{-1} — отражение.

LaTeX

$$$cs.IsReflection t \\Rightarrow cs.IsReflection t^{-1}$$$

Lean4

theorem isReflection_simple (i : B) : cs.IsReflection (s i) := by use 1, i; simp

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

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

Разделы

Аффилиация

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