iterate_map_div — Mathlib

English

Iterating a group endomorphism respects division: f^[n](x/y) = f^[n](x)/f^[n](y).

Русский

Итерация эндоморфизма сохраняет деление: f^[n](x/y) = f^[n](x)/f^[n](y).

LaTeX

$$$f^{[n]}\\left(\\frac{x}{y}\\right) = \\frac{f^{[n]}(x)}{f^{[n]}(y)}.$$$

Lean4

@[to_additive (attr := simp)]
theorem iterate_map_div {M F : Type*} [Group M] [FunLike F M M] [MonoidHomClass F M M] (f : F) (n : ℕ) (x y : M) :
    f^[n] (x / y) = f^[n] x / f^[n] y :=
  Semiconj₂.iterate (map_div f) n x y

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