toAdd_zpow — Mathlib

English

Let a be an element of the multiplicative version of the integers and b an integer. Then the additive image of a^b equals the product of the additive image of a and b: toAdd(a^b) = toAdd(a) · b.

Русский

Пусть a принадлежит мультипликативной структуре целых чисел, и b — целое число. Тогда аддитивное образование a^b равно произведению аддитивного образования a и b: toAdd(a^b) = toAdd(a) · b.

LaTeX

$$$ \operatorname{toAdd}(a^b) = \operatorname{toAdd}(a) \cdot b $$$

Lean4

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

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