English
The right inversion sequence satisfies a concatenation rule: ris(ω.concat i) equals the map-conjugate of ris(ω) concatenated with s_i.
Русский
Правильная последовательность инверсий удовлетворяет правилу конкатенации: ris(ω.concat i) = (π ω)⁻¹ s_i (π ω) multiplied в ris(ω) и затем ∎
LaTeX
$$$cs.rightInvSeq(\omega \concat i) = (List.map (MulAut.conj (s i)) (cs.rightInvSeq \omega)).concat (s i)$$$
Lean4
theorem rightInvSeq_concat (ω : List B) (i : B) :
ris(ω.concat i) = (List.map (MulAut.conj (s i)) (ris ω)).concat (s i) := by
induction ω with
| nil => simp
| cons j ω ih =>
dsimp [rightInvSeq, concat]
rw [ih]
simp only [concat_eq_append, wordProd_append, wordProd_cons, wordProd_nil, mul_one, mul_inv_rev, inv_simple,
cons.injEq, and_true]
group
