English
Let f be a monoid homomorphism, with G a group and H a division monoid. Then for any g ∈ G and n ∈ ℤ, f(g^n) = f(g)^n.
Русский
Пусть f — моноидный гомоморфизм, G — группа, H — дивизионный моноид. Тогда для любого g ∈ G и n ∈ ℤ выполняется f(g^n) = f(g)^n.
LaTeX
$$$$ \forall g \in G,\ \forall n \in \mathbb{Z},\ f(g^n) = f(g)^n. $$$$
Lean4
/-- Group homomorphisms preserve integer power.
See note [hom simp lemma priority] -/
@[to_additive (attr := simp mid) (reorder := 9 10) /-- Additive group homomorphisms preserve integer scaling. -/
]
theorem map_zpow [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g : G) (n : ℤ) : f (g ^ n) = f g ^ n :=
map_zpow' f (map_inv f) g n
