mapRangeRingHom_comp — Mathlib

English

Composition commutes: mapRangeRingHom M (f ∘ g) = (mapRangeRingHom M f) ∘ (mapRangeRingHom M g).

Русский

Сложение гомоморфизмов сохраняется: mapRangeRingHom M (f ∘ g) = (mapRangeRingHom M f) ∘ (mapRangeRingHom M g).

LaTeX

$$$ mapRangeRingHom\ M\ (f.comp\ g) = (mapRangeRingHom\ M\ f) .comp (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
      -- `MonoidAlgebra.of` doesn't translate with `to_additive`, so instead
      -- we have to tag these declarations with `to_additive existing`

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