toAdd_zpow — Mathlib

English

Let α be a type with a SubNegMonoid structure. For any a in Multiplicative α and any integer z, the additive version of a^z equals z times a (viewed additively).

Русский

Пусть α — множество с подмножеством SubNegMonoid. Для любого a из Multiplicative α и любого z ∈ ℤ имеет место равенство (a^z).toAdd = z · a.toAdd.

LaTeX

$$$\forall {\alpha} [\mathrm{SubNegMonoid}\ (\alpha)]\ (a : \mathrm{Multiplicative}\ \alpha)\ (z : \mathbb{Z}),\ (a^z).toAdd = z \cdot a.toAdd$$$

Lean4

@[simp]
theorem toAdd_zpow [SubNegMonoid α] (a : Multiplicative α) (z : ℤ) : (a ^ z).toAdd = z • a.toAdd :=
  rfl

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