Congruence_Relation_induces_Normal_Subgroup
Provedcongruence-relationsnormal-subgroupsproofwiki
A congruence relation on a group induces a normal subgroup.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Congruence_Relation_induces_Normal_Subgroup {G : Type _} [Group G] (N : Subgroup G) (hN : N.Normal) (a b g : G) (hab : a⁻¹ * b ∈ N) : (g * a)⁻¹ * (g * b) ∈ N := by sorrySource