map_comp — Mathlib

English

For ring homomorphisms f: R→S and g: S→T, the map on power series satisfies map(g∘f) = (map g) ∘ (map f).

Русский

Для гомоморфизмов f: R→S и g: S→T верно, что отображение на степенные ряды сохраняет композицию: map(g∘f) = (map g) ∘ (map f).

LaTeX

$$$\mathrm{PowerSeries.map}(g\circ f) = (\mathrm{PowerSeries.map}\, g) \circ (\mathrm{PowerSeries.map}\, f)$$$

Lean4

theorem map_comp : map (g.comp f) = (map g).comp (map f) :=
  rfl

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