reverse_mul — Mathlib

English

The reverse of a product is the product of reverses in reverse order: (l · m)^{reverse} = m^{reverse} · l^{reverse}.

Русский

Обратный образ произведения равен произведению обратных в обратном порядке: (l · m)^{reverse} = m^{reverse} · l^{reverse}.

LaTeX

$$$(l \\cdot m)^{\\ast} = m^{\\ast} \\cdot l^{\\ast}$$$

Lean4

@[simp]
theorem reverse_mul (l m : Language α) : (l * m).reverse = m.reverse * l.reverse :=
  by
  simp only [mul_def, reverse_eq_image, image2_image_left, image2_image_right, image_image2, List.reverse_append]
  apply image2_swap

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