GroupHom

structure GroupHom[G: Group, H: Group] {
    hom: G -> H
} constraint {
    is_hom(hom)
}

A group homomorphism that preserves the group structure.

GitHub

---

hom

GroupHom.hom: (GroupHom[G, H], G) -> H

The mapping for the homomorphism.