Theorems · Definition · group theory

AddMonoidHom.ker

{G : Type u_1} → [inst : AddGroup G] → {M : Type u_7} → [inst_1 : AddZeroClass M] → (G →+ M) → AddSubgroup G

The additive kernel of an AddMonoid homomorphism is the AddSubgroup of elements such that f x = 0

Defined in

Mathlib.Algebra.Group.Subgroup.Ker

Cited by

158 results in Mathlib

Foundations

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

Assumes

AddGroupAddZeroClass