inv

Mathlib.GroupTheory.Coxeter.Inversion

URI: https://scilib.ai/kg/mathlib#CoxeterSystem.IsReflection.inv

English

For any reflection t, t^2 = 1.

Русский

Для любого отражения t верно t^2 = 1.

LaTeX

$$$t^2 = 1$$$

Lean4

theorem inv : t⁻¹ = t := by
  rcases ht with ⟨w, i, rfl⟩
  simp [mul_assoc]

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

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

Разделы

Аффилиация

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