odd_length

Mathlib.GroupTheory.Coxeter.Inversion

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

← MathLib Explorer

English

If t is a reflection, then its length parity is odd, i.e., ℓ(t) is odd.

Русский

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

LaTeX

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

Lean4

theorem odd_length : Odd (ℓ t) :=
  by
  suffices cs.lengthParity t = Multiplicative.ofAdd 1 by
    simpa [lengthParity_eq_ofAdd_length, ZMod.natCast_eq_one_iff_odd]
  rcases ht with ⟨w, i, rfl⟩
  simp [lengthParity_simple]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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