normal_ker — Mathlib

English

The kernel of a group homomorphism is a normal subgroup of the domain.

Русский

Ядро гомоморфизма группы является нормальной подгруппой области определения.

LaTeX

$$$\ker f \trianglelefteq G$$$

Lean4

@[to_additive]
instance (priority := 100) normal_ker (f : G →* M) : f.ker.Normal :=
  ⟨fun x hx y => by rw [mem_ker, map_mul, map_mul, mem_ker.1 hx, mul_one, map_mul_eq_one f (mul_inv_cancel y)]⟩

Похожие утверждения