zpow_mulLeft — Mathlib

English

The z-powers of the left translation by a satisfy (addLeft(a))^n = addLeft(n a) for all n ∈ Z.

Русский

Z-степени левой трансляции на a удовлетворяют (addLeft(a))^n = addLeft(n a) для всех n ∈ Z.

LaTeX

$$$$ \\forall n \\in \\mathbb{Z},\\ (\\mathrm{addLeft}(a))^{n} = \\mathrm{addLeft}(n a). $$$$

Lean4

@[simp]
theorem zpow_mulLeft (n : ℤ) : Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n) :=
  (map_zpow ({ toFun := Equiv.mulLeft, map_one' := mulLeft_one, map_mul' := mulLeft_mul } : α →* Perm α) _ _).symm

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