English
The braidWord expressions for i,i' yield equal products; the two alternating words satisfy a braid relation.
Русский
Произведения braidWord для i,i' равны; чередующие слова удовлетворяют braid-отношению.
LaTeX
$$$\\\\pi(\\\\text{braidWord}(M, i, i')) = \\\\pi(\\\\text{braidWord}(M, i', i))$$$
Lean4
theorem prod_alternatingWord_eq_prod_alternatingWord_sub (i i' : B) (m : ℕ) (hm : m ≤ M i i' * 2) :
π(alternatingWord i i' m) = π(alternatingWord i' i (M i i' * 2 - m)) :=
by
simp_rw [prod_alternatingWord_eq_mul_pow, ← Int.even_coe_nat]
/- Rewrite everything in terms of an integer m' which is equal to m.
The resulting equation holds for all integers m'. -/
simp_rw [← zpow_natCast, Int.natCast_ediv, Int.ofNat_sub hm]
generalize (m : ℤ) = m'
clear hm
push_cast
rcases Int.even_or_odd' m' with ⟨k, rfl | rfl⟩
· rw [if_pos (by use k; ring), if_pos (by use -k + (M i i'); ring), mul_comm 2 k, ← sub_mul]
repeat rw [Int.mul_ediv_cancel _ (by simp)]
rw [zpow_sub, zpow_natCast, simple_mul_simple_pow' cs i i', ← inv_zpow]
simp
· have : ¬Even (2 * k + 1) := Int.not_even_iff_odd.2 ⟨k, rfl⟩
rw [if_neg this]
have : ¬Even (↑(M i i') * 2 - (2 * k + 1)) := Int.not_even_iff_odd.2 ⟨↑(M i i') - k - 1, by ring⟩
rw [if_neg this]
rw [(by ring : ↑(M i i') * 2 - (2 * k + 1) = -1 + (-k + ↑(M i i')) * 2), (by ring : 2 * k + 1 = 1 + k * 2)]
repeat rw [Int.add_mul_ediv_right _ _ (by simp)]
norm_num
rw [zpow_add, zpow_add, zpow_natCast, simple_mul_simple_pow', zpow_neg, ← inv_zpow, zpow_neg, ← inv_zpow]
simp [← mul_assoc]
