mapRingHom_comp — Mathlib

English

The mapping that maps coefficients composes: (mapRingHom f) ∘ (mapRingHom g) = mapRingHom (f ∘ g).

Русский

Отображение сопоставления коэффициентов сохраняет композицию: (mapRingHom f) ∘ (mapRingHom g) = mapRingHom (f ∘ g).

LaTeX

$$$\\,(\\mathrm{mapRingHom} f) \\circ (\\mathrm{mapRingHom} g) = \\mathrm{mapRingHom}(f \\circ g)\\, $$$

Lean4

@[simp]
theorem mapRingHom_comp [Semiring T] (f : S →+* T) (g : R →+* S) :
    (mapRingHom f).comp (mapRingHom g) = mapRingHom (f.comp g) :=
  RingHom.ext <| Polynomial.map_map g f

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