toMul_zsmul — Mathlib

English

For any DivInvMonoid α, z ∈ ℤ, and a ∈ Additive α, the multiplicative image of z-scalar a equals the z-th power of the multiplicative image of a: toMul(z · a) = (toMul(a))^z.

Русский

Для любого DivInvMonoid α, z ∈ ℤ и a ∈ Additive α: toMul(z · a) = (toMul(a))^z.

LaTeX

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

Lean4

@[simp]
theorem toMul_zsmul [DivInvMonoid α] (z : ℤ) (a : Additive α) : (z • a).toMul = a.toMul ^ z :=
  rfl

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