English
The congruence generated by a normal subgroup equals the kernel congruence of the quotient map.
Русский
Конгруэнтность, порождаемая нормальной подгруппой, равна конгруэнтности ядра отображения на факторгруппу.
LaTeX
$$Con f.ker = QuotientGroup.con f.ker$$
Lean4
/-- The congruence relation generated by a normal subgroup. -/
@[to_additive /-- The additive congruence relation generated by a normal additive subgroup. -/
]
protected def con : Con G where
toSetoid := leftRel N
mul' := fun {a b c d} hab hcd => by
rw [leftRel_eq] at hab hcd ⊢
dsimp only
calc
c⁻¹ * (a⁻¹ * b) * c⁻¹⁻¹ * (c⁻¹ * d) ∈ N := N.mul_mem (nN.conj_mem _ hab _) hcd
_ = (a * c)⁻¹ * (b * d) := by simp only [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
