iterate_map_mul — Mathlib

English

If f is a multiplicative endomorphism, then its n-th iterate preserves multiplication: f^[n](xy) = f^[n](x) f^[n](y).

Русский

Если f — мультипликативный эндоморфизм, то его n-ая итерация сохраняет умножение: f^[n](xy) = f^[n](x) f^[n](y).

LaTeX

$$$f^{[n]}(xy) = f^{[n]}(x)\\,f^{[n]}(y).$$$

Lean4

@[to_additive (attr := simp)]
theorem iterate_map_mul {M F : Type*} [Mul M] [FunLike F M M] [MulHomClass F M M] (f : F) (n : ℕ) (x y : M) :
    f^[n] (x * y) = f^[n] x * f^[n] y :=
  Function.Semiconj₂.iterate (map_mul f) n x y

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