ofMul_zpow — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem ofMul_zpow [DivInvMonoid α] (z : ℤ) (a : α) : ofMul (a ^ z) = z • ofMul a :=
  rfl

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