Skip to main content

RingHom

structure RingHom[R: Ring, S: Ring] {
    hom: R -> S
} constraint {
    is_ring_hom(hom)
}

A ring homomorphism that preserves both addition and multiplication and the multiplicative identity.

GitHub

ext​

let ext = ring_hom_ext[R, S]

Ring homomorphism extensionality from pointwise equality of the homomorphism.

hom​

RingHom.hom: (RingHom[R, S], R) -> S

The mapping for the homomorphism.