Theorems · Theorem · group theory

injective_iff_map_eq_one

∀ {F : Type u_7} {G : Type u_8} {H : Type u_9} [inst : Group G] [inst_1 : MulOneClass H] [inst_2 : FunLike F G H]
  [MonoidHomClass F G H] (f : F), Function.Injective ⇑f ↔ ∀ (a : G), f a = 1 → a = 1

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'.

Defined in

Mathlib.Algebra.Group.Hom.Basic

Cited by

9 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext

Assumes

GroupMulOneClassFunLikeMonoidHomClass