English
A homomorphism from a group to a monoid is injective iff its kernel is trivial: f(a) = 1 implies a = 1.
Русский
Гомоморфизм группы в моноид инъективен тогда и только тогда, когда его ядро тривиально: f(a) = 1 ведет к a = 1.
LaTeX
$$$\operatorname{Injective}(f) \iff \forall a, f(a) = 1 \Rightarrow a = 1$$$
Lean4
/-- A homomorphism from a group to a monoid is injective iff its kernel is trivial.
For the iff statement on the triviality of the kernel, see `injective_iff_map_eq_one'`. -/
@[to_additive /-- A homomorphism from an additive group to an additive monoid is injective iff
its kernel is trivial. For the iff statement on the triviality of the kernel,
see `injective_iff_map_eq_zero'`. -/
]
theorem _root_.injective_iff_map_eq_one {G H} [Group G] [MulOneClass H] [FunLike F G H] [MonoidHomClass F G H] (f : F) :
Function.Injective f ↔ ∀ a, f a = 1 → a = 1 :=
⟨fun h _ => (map_eq_one_iff f h).mp, fun h x y hxy =>
mul_inv_eq_one.1 <| h _ <| by rw [map_mul, hxy, ← map_mul, mul_inv_cancel, map_one]⟩
