prod_comp — Mathlib

English

The product of two AlgHoms respects composition: (g × g').comp f = (g.comp f) × (g'.comp f).

Русский

Произведение двух гомоморфизмов сохраняет композицию: (g × g') ∘ f = (g ∘ f) × (g' ∘ f).

LaTeX

$$$$ (g.\mathrm{prod}\, g').\mathrm{comp} \, f = (g.\mathrm{comp} \, f).\mathrm{prod} (g'.\mathrm{comp} \, f). $$$$

Lean4

theorem prod_comp {C' : Type*} [Semiring C'] [Algebra R C'] (f : A →ₐ[R] B) (g : B →ₐ[R] C) (g' : B →ₐ[R] C') :
    (g.prod g').comp f = (g.comp f).prod (g'.comp f) :=
  rfl

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