Homomorphism_of_Generated_Group
Provedgeneratorsgroup-theoryhomomorphismproofwiki
If two group homomorphisms phi, psi: G -> H agree on a generating set S of G, then phi = psi.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Homomorphism_of_Generated_Group {G H : Type _} [Group G] [Group H] (phi psi : G →* H) (S : Set G) (hgen : Subgroup.closure S = ⊤) (heq : ∀ s ∈ S, phi s = psi s) : phi = psi := by sorrySource