map_algebraMap_eq_subst_X — Mathlib

English

For any algebra map from R to S and any f in R⟦X⟧, applying the algebra map to f equals substituting X into f.

Русский

Для любого алгебраического отображения из R в S и любого f в R⟦X⟧ применение алгебраического отображения к f эквивалентно подстановке X в f.

LaTeX

$$$\\operatorname{map}(\\operatorname{algebraMap}\n R\\ S)\, f = \\operatorname{subst}\ X\\, f$$$

Lean4

theorem map_algebraMap_eq_subst_X (f : R⟦X⟧) : map (algebraMap R S) f = subst X f :=
  MvPowerSeries.map_algebraMap_eq_subst_X f

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