reduce_invRev_left_cancel — Mathlib

English

Reduction of inverse-reverse with left cancellation yields the empty word: reduce (invRev L ++ L) = [].

Русский

Редукция invRev(L) с левой стороны от L даёт пустое слово: reduce (invRev L ++ L) = [].

LaTeX

$$$\forall L : List(Prod\;\alpha\;Bool),\; \mathrm{reduce}(\mathrm{invRev} L ++ L) = []$$$

Lean4

@[to_additive]
theorem reduce_invRev_left_cancel : reduce (invRev L ++ L) = [] := by simp [← toWord_mk, ← mul_mk, ← inv_mk]

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