zpow_apply_eq_self_of_apply_eq_self

English

If f fixes x, then every integer power (including negative powers) fixes x as well: (f^n)x = x for all n ∈ ℤ.

Русский

Если f фиксирует x, то для любого целого n: (f^n)x = x.

LaTeX

$$$\forall x:\alpha,\ f(x)=x \Rightarrow \forall n:\mathbb{Z},\ (f^n)x=x$$$

Lean4

theorem zpow_apply_eq_self_of_apply_eq_self {x : α} (hfx : f x = x) : ∀ n : ℤ, (f ^ n) x = x
  | (n : ℕ) => pow_apply_eq_self_of_apply_eq_self hfx n
  | Int.negSucc n => by rw [zpow_negSucc, inv_eq_iff_eq, pow_apply_eq_self_of_apply_eq_self hfx]

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