ofLex_pow — Mathlib

English

Let α be a type with a power operation. For all a in α and b in β, the ofLex map distributes over exponentiation: ofLex(a^b) = (ofLex a)^b.

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) ofLex_smul]
theorem ofLex_pow [Pow α β] (a : Lex α) (b : β) : ofLex (a ^ b) = ofLex a ^ b :=
  rfl

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