English
There is a length parity homomorphism lengthParity from W to the multiplicative group of Z/2Z, sending each w to the parity of its length.
Русский
Существует отображение паритета длины lengthParity: W → Multiplicative(Z/2Z), отправляющее каждый элемент w в паритет длины ℓ(w).
LaTeX
$$$\\\\text{lengthParity}: W \\to^* \\text{Multiplicative}(\\\\mathbb{Z}/2\\\\mathbb{Z})$ with \\\\text{lengthParity}(w) \\equiv \\\\ell(w) \\\\\\mathrm{mod} \\\\;2$$$
Lean4
/-- The homomorphism that sends each element `w : W` to the parity of the length of `w`.
(See `lengthParity_eq_ofAdd_length`.) -/
def lengthParity : W →* Multiplicative (ZMod 2) :=
cs.lift
⟨fun _ ↦ Multiplicative.ofAdd 1,
by
simp_rw [CoxeterMatrix.IsLiftable, ← ofAdd_add, (by decide : (1 + 1 : ZMod 2) = 0)]
simp⟩
