MonoidHom

structure MonoidHom[M: Monoid, N: Monoid] {
    hom: M -> N
} constraint {
    is_monoid_hom(hom)
}

A monoid homomorphism that preserves the operation and the identity.

GitHub

---

ext

let ext = monoid_hom_ext[M, N]

Monoid homomorphism extensionality from pointwise equality of the homomorphism.

hom

MonoidHom.hom: (MonoidHom[M, N], M) -> N

The mapping for the homomorphism.