Theorems · Definition · group theory

AddMonoidHom.eqLocusM

{M : Type u_1} →
  {N : Type u_2} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → (M →+ N) → (M →+ N) → AddSubmonoid M

The additive submonoid of elements x : M such that f x = g x

Defined in

Mathlib.Algebra.Group.Submonoid.Defs

Cited by

6 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext

Assumes

AddZeroClassAddZeroClass