algHom_comp — Mathlib

English

Pi-algHom commutes with composition: (Pi.algHom g).comp h = Pi.algHom g' where g' i = (g_i).comp h.

Русский

Pi-algHom коммутирует с композициями: (Pi.algHom g).comp h = Pi.algHom g', где g'_i = (g_i).comp h.

LaTeX

$$$ (\\mathrm{algHom}\\,R\\,A\\, g).comp h = \\mathrm{algHom}\\,R\\,A\\, (\\lambda i, (g_i).comp h) $$$

Lean4

/-- `Pi.algHom` commutes with composition. -/
theorem algHom_comp {B C : Type*} [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (g : ∀ i, C →ₐ[R] A i)
    (h : B →ₐ[R] C) : (algHom R A g).comp h = algHom R A (fun i ↦ (g i).comp h) :=
  rfl

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