exists_reduced_word — Mathlib

English

For every w in the group, there exists a word ω such that ω.length = ℓ(w) and w = π ω; i.e., every element has a reduced word representation.

Русский

Для каждого w в группе существует слово ω такое, что ω.length = ℓ(w) и w = π ω; то есть у каждого элемента есть сокращённое представление словом.

LaTeX

$$$\exists \omega, \omega.length = \ell w \wedge w = \pi \omega$$$

Lean4

theorem exists_reduced_word (w : W) : ∃ ω, ω.length = ℓ w ∧ w = π ω := by
  classical
  have := Nat.find_spec (cs.exists_word_with_prod w)
  tauto

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