zpow_mulRight — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem zpow_mulRight : ∀ n : ℤ, Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n)
  | Int.ofNat n => by simp
  | Int.negSucc n => by simp

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