English
The kernel of the quotient map induced by a congruence on a monoid M equals that congruence; i.e., ker (c.mk) = c.
Русский
Ядро отображения-квартирования, индуцированного конгруэнцией на моноиде M, совпадает с самой конгруэнцией: ker (c.mk) = c.
LaTeX
$$$\ker (c.mk) = c$$$
Lean4
/-- Given a monoid homomorphism `f` from `M` to `P`, the kernel of `f` is the unique congruence
relation on `M` whose induced map from the quotient of `M` to `P` is injective. -/
@[to_additive /-- Given an `AddMonoid` homomorphism `f` from `M` to `P`, the kernel of `f`
is the unique additive congruence relation on `M` whose induced map from the quotient of `M`
to `P` is injective. -/
]
theorem ker_eq_lift_of_injective (H : c ≤ ker f) (h : Injective (c.lift f H)) : ker f = c :=
toSetoid_inj <| Setoid.ker_eq_lift_of_injective f H h
