English
The products of two alternating words of length M_ii' with i,i' alternate agree; expressing the braid relation.
Русский
Произведения двух чередующихся слов одинаковы — braid-отношение в явном виде.
LaTeX
$$$\\\\pi(\\\\text{braidWord}(M, i, i')) = \\\\pi(\\\\text{braidWord}(M, i', i))$$$
Lean4
/-- The two words of length `M i i'` that alternate between `i` and `i'` have the same product.
This is known as the "braid relation" or "Artin-Tits relation". -/
theorem wordProd_braidWord_eq (i i' : B) : π(braidWord M i i') = π(braidWord M i' i) :=
by
have := cs.prod_alternatingWord_eq_prod_alternatingWord_sub i i' (M i i') (Nat.le_mul_of_pos_right _ (by simp))
rw [tsub_eq_of_eq_add (mul_two (M i i'))] at this
nth_rw 2 [M.symmetric i i'] at this
exact this
