prod — Mathlib

English

The Pi.prod of two AlgHoms is an AlgHom to the product, with behavior on components given by the respective rings.

Русский

Произведение Pi.prod двух AlgHom даёт AlgHom в произведение, действующий по компонентам соответствующих колец.

LaTeX

$$$$ (f \prod g) : A \to_R B \times C $$$$

Lean4

/-- The `Pi.prod` of two morphisms is a morphism. -/
@[simps!]
def prod (f : A →ₐ[R] B) (g : A →ₐ[R] C) : A →ₐ[R] B × C :=
  { f.toRingHom.prod g.toRingHom with
    commutes' := fun r => by
      simp only [toRingHom_eq_coe, RingHom.toFun_eq_coe, RingHom.prod_apply, coe_toRingHom, commutes,
        Prod.algebraMap_apply] }

Похожие утверждения