map_powers — Mathlib

English

A monoid hom f preserves powers: the image of powers(m) under f equals powers of f(m).

Русский

Гомоморфизм f сохраняет степени: образ степеней(m) равен степеням f(m).

LaTeX

$$$ (\\operatorname{powers}(m)).map f = \\operatorname{powers}(f(m)) $$$

Lean4

@[simp]
theorem map_powers {N : Type*} {F : Type*} [Monoid N] [FunLike F M N] [MonoidHomClass F M N] (f : F) (m : M) :
    (powers m).map f = powers (f m) := by simp only [powers_eq_closure, map_mclosure f, Set.image_singleton]

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