zpow_addRight — 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_addRight : ∀ (n : ℤ), Equiv.addRight a ^ n = Equiv.addRight (n • a)
  | Int.ofNat n => by simp
  | Int.negSucc n => by simp

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