Skip to main content

AddCommGroupHom

structure AddCommGroupHom[A: AddCommGroup, B: AddCommGroup] {
    hom: A -> B
} constraint {
    is_add_comm_group_hom(hom)
}

An additive commutative group homomorphism.

GitHub

ext​

let ext = add_comm_group_hom_ext[A, B]

Additive commutative group homomorphism extensionality from pointwise equality of the mapping.

hom​

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

The mapping of the additive commutative group homomorphism.