English
The product map induces a ring hom structure on End rings: prodMapRingHom maps a pair of endomorphisms to an endomorphism on the product, respecting the ring operations.
Русский
Произведение отображений порождает структуру кольцевого однородника на концевых отображениях: prodMapRingHom переводит пару концевых отображений в концевое на произведении и сохраняет кольцевые операции.
LaTeX
$$$ \\text{prodMapRingHom} : (End_R M \\times End_R M_2) \\to+* End_R(M \\times M_2) $$$
Lean4
/-- `LinearMap.prodMap` as a `RingHom` -/
@[simps]
def prodMapRingHom : (M →ₗ[R] M) × (M₂ →ₗ[R] M₂) →+* M × M₂ →ₗ[R] M × M₂
where
toFun f := prodMap f.1 f.2
map_one' := prodMap_one
map_zero' := rfl
map_add' _ _ := rfl
map_mul' _ _ := rfl
