Kernel_is_Normal_Subgroup_of_Domain
Provedgroup-homomorphismskernelsnormal-subgroupsproofwiki
The kernel of a group homomorphism is a normal subgroup.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Kernel_is_Normal_Subgroup_of_Domain {G₁ G₂ : Type _} [Group G₁] [Group G₂] (φ : MonoidHom G₁ G₂) (g h : G₁) (hh : φ h = 1) : φ (g * h * g⁻¹) = 1 := by sorrySource
Human review