English
Let f be a monoid homomorphism with hf: ∀ x ∈ G, f(x⁻¹) = f(x)⁻¹. Then for all a ∈ G and n ∈ ℤ, f(a^n) = f(a)^n.
Русский
Пусть f — моноидный гомоморфизм с условием hf: ∀ x ∈ G, f(x⁻¹) = f(x)⁻¹. Тогда для любого a ∈ G и n ∈ ℤ выполняется f(a^n) = f(a)^n.
LaTeX
$$$$ \forall a \in G,\ \forall n \in \mathbb{Z},\ f(a^n) = f(a)^n. $$$$
Lean4
@[to_additive]
theorem map_zpow' [DivInvMonoid G] [DivInvMonoid H] [MonoidHomClass F G H] (f : F) (hf : ∀ x : G, f x⁻¹ = (f x)⁻¹)
(a : G) : ∀ n : ℤ, f (a ^ n) = f a ^ n
| (n : ℕ) => by rw [zpow_natCast, map_pow, zpow_natCast]
| Int.negSucc n => by rw [zpow_negSucc, hf, map_pow, ← zpow_negSucc]
