map_comp_zpow — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem map_comp_zpow [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g : ι → G) (n : ℤ) :
    f ∘ (g ^ n) = f ∘ g ^ n := by simp

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