English
For any ω and index j, the j-th component of the rightInvSeq of ω is given by a conjugate of the j-th element (if it exists) by the word π(ω.drop(j+1)) on both sides.
Русский
Для любых ω и индекса j j-й компонент правойInvSeq ω задаётся как сопряжение j-го элемента (если он существует) произведением π(ω.drop(j+1)) слева и справа.
LaTeX
$$$(\mathrm{ris}(\omega)).\mathrm{getD} \\; j \\; 1 = (\pi(\omega.drop(j+1)))^{-1} \cdot (\mathrm{Option.map}(\mathrm{cs.simple}) (\omega[j]?)).getD 1 \cdot \pi(\omega.drop(j+1))$$$
Lean4
theorem getD_rightInvSeq (ω : List B) (j : ℕ) :
(ris ω).getD j 1 = (π(ω.drop (j + 1)))⁻¹ * (Option.map (cs.simple) ω[j]?).getD 1 * π(ω.drop (j + 1)) := by
induction ω generalizing j with
| nil => simp
| cons i ω ih =>
dsimp only [rightInvSeq]
rcases j with _ | j'
· simp
· simp only [getD_eq_getElem?_getD] at ih
simp [ih j']
