zpow_addLeft — 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_addLeft (n : ℤ) : Equiv.addLeft a ^ n = Equiv.addLeft (n • a) :=
  (map_zsmul ({ toFun := Equiv.addLeft, map_zero' := addLeft_zero, map_add' := addLeft_add } : α →+ Additive (Perm α)) _
      _).symm

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