perm_zpow — Mathlib

English

If x is fixed by e, then x is fixed by e^n for all integers n, including negative powers.

Русский

Если x фиксирована e, то x фиксирована и для e^n при любых целых n, включая отрицательные степени.

LaTeX

$$$IsFixedPt e x \rightarrow \forall n:\mathbb{Z}, IsFixedPt (e^n) x$$$

Lean4

protected theorem perm_zpow (h : IsFixedPt e x) : ∀ n : ℤ, IsFixedPt (⇑(e ^ n)) x
  | Int.ofNat _ => h.perm_pow _
  | Int.negSucc n => (h.perm_pow <| n + 1).perm_inv

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