Group_Homomorphism_Preserves_Subgroups
Provedgroup-homomorphismsproofwikisubgroups
Group homomorphism preserves subgroups.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Group_Homomorphism_Preserves_Subgroups {G₁ G₂ : Type _} [Group G₁] [Group G₂] (φ : MonoidHom G₁ G₂) (H : Subgroup G₁) (h : G₁) (hh : h ∈ H) : φ h ∈ H.map φ := by sorrySource