mul_self

Mathlib.GroupTheory.Coxeter.Inversion

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

English

If t is a reflection, then the length ℓ(t) is odd.

Русский

Если t — отражение, то длина ℓ(t) нечётна.

LaTeX

$$$\\\\text{Odd}(\\\\ell(t))$$$

Lean4

theorem mul_self : t * t = 1 := by
  rcases ht with ⟨w, i, rfl⟩
  simp

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

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

Разделы

Аффилиация

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