theorem CoxeterSystem.neg_one_units_pow_eq_of_mod_two_eq {a b : ℕ} (h : a % 2 = b % 2) : (-1) ^ a = (-1) ^ b

Helper: $(-1)^a = (-1)^b$ in $\mathbb{Z}^\times$ whenever $a \equiv b \pmod 2$.

noncomputable def CoxeterSystem.paritySign {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : W →* ℤˣ

Parity sign homomorphism $\varepsilon : W \to \{\pm 1\}$ defined by $\varepsilon(w) = (-1)^{\ell(w)}$; well-defined because $\ell$ is well-defined modulo $2$ under multiplication.

@[simp]

theorem CoxeterSystem.paritySign_eq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) : cs.paritySign w = (-1) ^ cs.length w

Unfolding equation: $\varepsilon(w) = (-1)^{\ell(w)}$.