length_eq_one_iff — Mathlib

English

A word ω is reduced exactly when the length of the word's product equals the length of ω: IsReduced(ω) ⇔ ℓ(π ω) = ω.length.

Русский

Слово ω редуцировано тогда и только тогда, когда длина элемента π ω равна длине ω: IsReduced(ω) ⇔ ℓ(π ω) = |ω|.

LaTeX

$$$\\\\text{IsReduced}(\\\\omega) \\\\iff \\\\ell(\\\\pi \\\\omega) = |\\\\omega|$$$

Lean4

theorem length_eq_one_iff {w : W} : ℓ w = 1 ↔ ∃ i : B, w = s i :=
  by
  constructor
  · intro h
    rcases cs.exists_reduced_word w with ⟨ω, hω, rfl⟩
    rcases List.length_eq_one_iff.mp (hω.trans h) with ⟨i, rfl⟩
    exact ⟨i, cs.wordProd_singleton i⟩
  · rintro ⟨i, rfl⟩
    exact cs.length_simple i

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