lengthParity_eq_ofAdd_length — Mathlib

English

For any w in W, lengthParity(w) equals ofAdd(ℓ(w)) in Z/2Z, i.e., the parity of ℓ(w).

Русский

Для любого w в W паритет длины равен преобразованию ℓ(w) по модулю 2: lengthParity(w) = ofAdd(ℓ(w)).

LaTeX

$$$\\\\text{lengthParity}(w) = \\\\overline{\\\\ell(w)} \in \\\\mathbb{Z}/2\\\\mathbb{Z}$$$

Lean4

theorem lengthParity_eq_ofAdd_length (w : W) : cs.lengthParity w = Multiplicative.ofAdd (↑(ℓ w)) :=
  by
  rcases cs.exists_reduced_word w with ⟨ω, hω, rfl⟩
  rw [← hω, wordProd, map_list_prod, List.map_map, lengthParity_comp_simple, map_const', prod_replicate, ← ofAdd_nsmul,
    nsmul_one]

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