Theorems · Definition · group theory

AddMonoidHom.eqLocus

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

The additive subgroup of elements x : G such that f x = g x

Defined in

Mathlib.Algebra.Group.Subgroup.Ker

Cited by

2 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext

Assumes

AddGroupAddMonoid