reverse_pow

Mathlib.Computability.Language

URI: https://scilib.ai/kg/mathlib#Language.reverse_pow

English

The reverse of a power is the power of the reverse: (l^n)^{reverse} = (l.reverse)^n.

Русский

Разворот степени равен степени разворота: (l^n)^{reverse} = (l.reverse)^n.

LaTeX

$$$(l^{n})^{\\text{reverse}} = (l^{\\text{reverse}})^{n}$$$

Lean4

@[simp]
theorem reverse_pow (l : Language α) (n : ℕ) : (l ^ n).reverse = l.reverse ^ n :=
  MulOpposite.op_injective (map_pow (reverseIso α) l n)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru