prod_rightInvSeq — Mathlib

English

The product of the elements of the rightInvSeq of ω equals the inverse of the word π ω; similarly for leftInvSeq.

Русский

Произведение элементов rightInvSeq ω равно обратному произведению слова π ω; аналогично для leftInvSeq.

LaTeX

$$$\mathrm{prod}(\mathrm{ris}(\omega)) = (\pi(\omega))^{-1}$ and $\mathrm{prod}(\mathrm{lis}(\omega)) = (\pi(\omega))^{-1}$$$

Lean4

theorem prod_rightInvSeq (ω : List B) : prod (ris ω) = (π ω)⁻¹ := by
  induction ω with
  | nil => simp
  | cons i ω ih => simp [rightInvSeq, ih, wordProd_cons]

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