English
For ω and j, the j-th element of the rightInvSeq ω equals the same conjugate expression as in GetD, i.e., it is the corresponding product of π and the conjugated simple reflections.
Русский
Для ω и j j-й элемент правойInvSeq ω равен тому же выражению сопряжения, как в GetD, то есть соответствующий произведению π и сопряжённых простых отражений.
LaTeX
$$$(\mathrm{ris}(\omega))[j]' = (\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 getElem_rightInvSeq (ω : List B) (j : ℕ) (h : j < ω.length) :
(ris ω)[j]'(by simp [h]) = (π(ω.drop (j + 1)))⁻¹ * (Option.map (cs.simple) ω[j]?).getD 1 * π(ω.drop (j + 1)) := by
rw [← List.getD_eq_getElem (ris ω) 1, getD_rightInvSeq]
