Theorems · Definition · group theory

MonoidHom.mgraph

{G : Type u_1} → {H : Type u_2} → [inst : Monoid G] → [inst_1 : Monoid H] → (G →* H) → Submonoid (G × H)

The graph of a monoid homomorphism as a submonoid. See also MonoidHom.graph for the graph as a subgroup.

Defined in

Mathlib.Algebra.Group.Graph

Cited by

8 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext

Assumes

MonoidMonoid