Homomorphism_of_Powers

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

homomorphismsproofwiki

Let $\struct {T_1, \odot}$ and $\struct {T_2, \oplus}$ be semigroups. Let $\phi: \struct {T_1, \odot} \to \struct {T_2, \oplus}$ be a (semigroup) homomorphism.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Homomorphism_of_Powers {M N : Type _} [Monoid M] [Monoid N] (f : M →* N) (x : M) (n : ℕ) : f (x ^ n) = (f x) ^ n := by sorry

Source

https://proofwiki.org/wiki/Homomorphism_of_Powers

View graph