toAdd_pow — Mathlib

English

For any DivInvMonoid α and z ∈ ℤ, the additive image of a^z under toMul equals z times the additive image of a: toMul(a^z) = z · ofMul(a).

Русский

Для любого DivInvMonoid α и z ∈ ℤ, образ от a^z через toMul равен z · образу от a: toMul(a^z) = z · ofMul(a).

LaTeX

$$$ \mathrm{toMul}(a^{z}) = z \cdot \mathrm{ofMul}(a) $$$

Lean4

@[simp]
theorem toAdd_pow [AddMonoid α] (a : Multiplicative α) (n : ℕ) : (a ^ n).toAdd = n • a.toAdd :=
  rfl

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