English
A group homomorphism f is injective iff the only element sent to 1 is the identity.
Русский
Гомоморфизм группы инъективен тогда и только тогда, когда единственный элемент, отображаемый в 1, — тождественный элемент.
LaTeX
$$$\forall a, f(a) = 1 \Rightarrow a = 1$$$
Lean4
/-- A homomorphism from a group to a monoid is injective iff its kernel is trivial,
stated as an iff on the triviality of the kernel.
For the implication, 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, stated as an iff on the triviality of the kernel. For the implication, 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 :=
(injective_iff_map_eq_one f).trans <| forall_congr' fun _ => ⟨fun h => ⟨h, fun H => H.symm ▸ map_one f⟩, Iff.mp⟩
