English
For any ω and j, the j-th diagonal element of the leftInvSeq ω is π(ω.take j) multiplied by the j-th optional simple reflection (if present), then multiplied by π(ω.take j)^{-1}.
Русский
Для любого ω и j j-й диагональный элемент lis ω задаётся как произведение π(ω.take j) на (ω[j]?) при наличии на элементе, умноженное на π(ω.take j)^{-1}.
LaTeX
$$$(\mathrm{lis}(\omega)).getD j 1 = \pi(\omega.take j) \cdot (\mathrm{Option.map}(\mathrm{cs.simple}) (\omega[j]?)).getD 1 \cdot (\pi(\omega.take j))^{-1}$$$
Lean4
theorem getD_leftInvSeq (ω : List B) (j : ℕ) :
(lis ω).getD j 1 = π(ω.take j) * (Option.map (cs.simple) ω[j]?).getD 1 * (π(ω.take j))⁻¹ := by
induction ω generalizing j with
| nil => simp
| cons i ω ih =>
dsimp [leftInvSeq]
rcases j with _ | j'
· simp
· rw [getD_cons_succ]
rw [(by simp : 1 = ⇑(MulAut.conj (s i)) 1)]
rw [getD_map]
rw [ih j']
simp [← mul_assoc, wordProd_cons]
