English
The product of the alternatingWord equals a piecewise power of simple reflections: (depending on parity) the identity and powers of s_i and s_i'.
Русский
Произведение чередующегося слова равно произведению простых отражений в зависимости от чётности: единица и степени элементов s_i, s_i'.
LaTeX
$$$\\\\pi(\\\\text{alternatingWord}(i, i', m)) = (\\\\text{If } m \\text{ even then } 1 \\text{ else } s_i') \\,\\\\cdot\\\\, (s_i s_i')^{m/2}$$$
Lean4
theorem prod_alternatingWord_eq_mul_pow (i i' : B) (m : ℕ) :
π(alternatingWord i i' m) = (if Even m then 1 else s i') * (s i * s i') ^ (m / 2) := by
induction m with
| zero => simp [alternatingWord]
| succ m ih =>
rw [alternatingWord_succ', wordProd_cons, ih]
by_cases hm : Even m
· have h₁ : ¬Even (m + 1) := by simp [hm, parity_simps]
have h₂ : (m + 1) / 2 = m / 2 := Nat.succ_div_of_not_dvd <| by rwa [← even_iff_two_dvd]
simp [hm, h₁, h₂]
· have h₁ : Even (m + 1) := by simp [hm, parity_simps]
have h₂ : (m + 1) / 2 = m / 2 + 1 := Nat.succ_div_of_dvd h₁.two_dvd
simp [hm, h₁, h₂, ← pow_succ', ← mul_assoc]
