toLex_pow — Mathlib

English

Let α be a type with a power operation. For all a in α and b in β, the embedding toLex preserves exponentiation: toLex(a^b) = (toLex a)^b.

Русский

Пусть α имеет операцию возведения в степень. Для всех a ∈ α и b ∈ β отображение toLex сохраняет возведение в степень: toLex(a^b) = (toLex a)^b.

LaTeX

$$$\operatorname{toLex}(a^{b}) = \operatorname{toLex}(a)^{b}$$$

Lean4

@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) toLex_smul]
theorem toLex_pow [Pow α β] (a : α) (b : β) : toLex (a ^ b) = toLex a ^ b :=
  rfl

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