map_comp_pow — Mathlib

English

Let f be a MonoidHom and g : ι → G. For n ∈ ℕ, f ∘ (g^n) = (f ∘ g)^n.

Русский

Пусть f — моноидный гомоморфизм, и g: ι → G. Для натурального n выполняется f ∘ (g^n) = (f ∘ g)^n.

LaTeX

$$$$ \forall ι,\ G,\ f: (\iota \to G)\ ,\forall n \in \mathbb{N},\ f \circ (g^n) = (f \circ g)^n. $$$$

Lean4

@[to_additive (attr := simp)]
theorem map_comp_pow [Monoid G] [Monoid H] [MonoidHomClass F G H] (f : F) (g : ι → G) (n : ℕ) :
    f ∘ (g ^ n) = f ∘ g ^ n := by ext; simp

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