getD_leftInvSeq_mul_wordProd — Mathlib

English

The product of the leftInvSeq ω, multiplied by the word product ω, equals the word product after erasing the j-th element from ω.

Русский

Произведение левойInvSeq ω, умноженное на произведение слова ω, равно произведению слова после стирания j-ого элемента ω.

LaTeX

$$$(\mathrm{leftInvSeq}(\omega)).\mathrm{prod} \cdot (\mathrm{wordProd}(\omega)) = \mathrm{wordProd}(\omega.eraseIdx j)$$$

Lean4

theorem getD_leftInvSeq_mul_wordProd (ω : List B) (j : ℕ) : ((lis ω).getD j 1) * π ω = π(ω.eraseIdx j) :=
  by
  rw [getD_leftInvSeq, eraseIdx_eq_take_drop_succ]
  nth_rw 4 [← 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

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