AddGroupHom

structure AddGroupHom[A: AddGroup, B: AddGroup] {
    hom: A -> B
} constraint {
    is_add_group_hom(hom)
}

An additive group homomorphism that preserves the additive group structure.

GitHub

---

ext

let ext = add_group_hom_ext[A, B]

Additive group homomorphism extensionality from pointwise equality of the homomorphism.

hom

AddGroupHom.hom: (AddGroupHom[A, B], A) -> B

The mapping for the homomorphism.