length_eq_zero_iff — Mathlib

English

Let cs be a Coxeter system for the matrix M and the group W. For every w in W, the length ℓ(w) is zero if and only if w equals the identity.

Русский

Пусть cs является системой Коксетера для матрицы M и группы W. Для каждого w в W выполняется: длина ℓ(w) равна нулю тогда и только тогда, когда w = 1.

LaTeX

$$$\\\\forall w \\,(w \in W):\\\\ell(w) = 0 \\\\iff w = 1$$$

Lean4

@[simp]
theorem length_eq_zero_iff {w : W} : ℓ w = 0 ↔ w = 1 :=
  by
  constructor
  · intro h
    rcases cs.exists_reduced_word w with ⟨ω, hω, rfl⟩
    have : ω = [] := eq_nil_of_length_eq_zero (hω.trans h)
    rw [this, wordProd_nil]
  · rintro rfl
    exact cs.length_one

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