wordProd_reverse — Mathlib

English

The product over the reverse of a word is the inverse of the product of the word.

Русский

Произведение слова в обратном порядке равно обратному произведению слова.

LaTeX

$$$\\\\pi(\\\\text{reverse}(\\\\omega)) = (\\\\pi(\\\\omega))^{-1}$$$

Lean4

@[simp]
theorem wordProd_reverse (ω : List B) : π(reverse ω) = (π ω)⁻¹ := by
  induction ω with
  | nil => simp
  | cons x ω' ih => simpa [wordProd_cons, wordProd_append] using ih

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