map_algebraMap_eq_subst_X — Mathlib

English

A standard relation equates map(algebraMap) with substitution by X: map(algebraMap) f = subst X f.

Русский

Стандартное соотношение: map(algebraMap) f = subst X f.

LaTeX

$$$\\operatorname{map}(\\operatorname{algebraMap})\\; f = \\operatorname{subst}(\\mathrm{X})\\; f$$$

Lean4

theorem map_algebraMap_eq_subst_X (f : MvPowerSeries σ R) : map (algebraMap R S) f = subst X f :=
  by
  ext e
  rw [coeff_map, coeff_subst HasSubst.X f e, finsum_eq_single _ e]
  · rw [← MvPowerSeries.monomial_one_eq, coeff_monomial_same, algebra_compatible_smul S, smul_eq_mul, mul_one]
  · intro d hd
    rw [← MvPowerSeries.monomial_one_eq, coeff_monomial_ne hd.symm, smul_zero]

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