toAdd_pow — Mathlib

English

Let a be a multiplicative integer and b a natural number. Then the additive image of a^b equals the additive image of a multiplied by b.

Русский

Пусть a ∈ Multiplicative ℤ и b ∈ ℕ. Тогда образ в аддитивной записи числа a^b равен произведению a в аддитивной записи на b.

LaTeX

$$$ (a^b).toAdd = a.toAdd \cdot b $$$

Lean4

theorem toAdd_pow (a : Multiplicative ℤ) (b : ℕ) : (a ^ b).toAdd = a.toAdd * b :=
  mul_comm _ _

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