Theorems · Definition · group theory

MonoidHom.ker

{G : Type u_1} → [inst : Group G] → {M : Type u_7} → [inst_1 : MulOneClass M] → (G →* M) → Subgroup G

The multiplicative kernel of a monoid homomorphism is the subgroup of elements x : G such that f x = 1

Defined in

Mathlib.Algebra.Group.Subgroup.Ker

Cited by

212 results in Mathlib

Foundations

Depth 17 from the axioms, rests on 112 definitions · uses propext

Assumes

GroupMulOneClass