English
The kernel of a monoid homomorphism f is the subgroup of all elements mapped to the identity.
Русский
Ядро монадообразного гомоморфизма f — это подгруппа всех элементов, которые отображаются в единицу.
LaTeX
$$$$ \\ker f = \\{ x \\in G \\mid f(x) = 1 \\} $$$$
Lean4
/-- The multiplicative kernel of a monoid homomorphism is the subgroup of elements `x : G` such that
`f x = 1` -/
@[to_additive /-- The additive kernel of an `AddMonoid` homomorphism is the `AddSubgroup` of elements
such that `f x = 0` -/
]
def ker (f : G →* M) : Subgroup G :=
{ MonoidHom.mker f with
inv_mem' := fun {x} (hx : f x = 1) =>
calc
f x⁻¹ = f x * f x⁻¹ := by rw [hx, one_mul]
_ = 1 := by rw [← map_mul, mul_inv_cancel, map_one] }
