mapRangeRingHom_comp — Mathlib

English

Composition of ring homomorphisms corresponds to the composition of the induced mapRangeRingHom maps on monoid algebras.

Русский

Сложение гомоморфизмов колец соответствует композиции отображений mapRangeRingHom на моноидной алгебре.

LaTeX

$$$mapRangeRingHom M (f \circ g) = (mapRangeRingHom M f) \circ (mapRangeRingHom M g)$$$

Lean4

@[simp]
theorem mapRangeRingHom_comp (f : S →+* T) (g : R →+* S) :
    mapRangeRingHom M (f.comp g) = (mapRangeRingHom M f).comp (mapRangeRingHom M g) := by ext <;> simp

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