iterate_map_inv — Mathlib

English

In a group, iterating a monoid hom preserves inverses: f^[n](x^{-1}) = (f^[n](x))^{-1}.

Русский

В группе итерация гомоморфизма сохраняет обратные: f^[n](x^{-1}) = (f^[n](x))^{-1}.

LaTeX

$$$f^{[n]}(x^{-1}) = (f^{[n]}(x))^{-1}.$$$

Lean4

@[to_additive (attr := simp)]
theorem iterate_map_inv {M F : Type*} [Group M] [FunLike F M M] [MonoidHomClass F M M] (f : F) (n : ℕ) (x : M) :
    f^[n] x⁻¹ = (f^[n] x)⁻¹ :=
  Commute.iterate_left (map_inv f) n x

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