wordProd_mul_getD_rightInvSeq — Mathlib

English

Multiplication by the right-inverse sequence deletes the j-th letter via eraseIdx.

Русский

Умножение на правую инверсионную последовательность стирает j-ю букву через eraseIdx.

LaTeX

$$$\\pi(\\omega) * ((\\mathrm{ris}(\\omega)).getD\\; j\\; 1) = \\pi(\\omega.\\eraseIdx j)$$$

Lean4

theorem wordProd_mul_getD_rightInvSeq (ω : List B) (j : ℕ) : π ω * ((ris ω).getD j 1) = π(ω.eraseIdx j) :=
  by
  rw [getD_rightInvSeq, eraseIdx_eq_take_drop_succ]
  nth_rw 1 [← take_append_drop (j + 1) ω]
  rw [take_succ]
  obtain lt | le := lt_or_ge j ω.length
  · simp only [getElem?_eq_getElem lt, wordProd_append, mul_assoc]
    simp
  · simp only [getElem?_eq_none le]
    simp

Похожие утверждения