English
A general identity for monomials: the monomial e with coefficient ∏ r_s^{e(s)} equals ∏ (r_s•X_s)^{e(s)}.
Русский
Общее тождество для мономиалов: мономиал e с коэффициентом ∏ r_s^{e(s)} равен ∏ (r_s • X_s)^{e(s)}.
LaTeX
$$$\\mathrm{MvPowerSeries.monomial}(e, e.prod_{s} r(s)^{e(s)}) = \\prod_s ( r(s) \\cdot \\mathrmMvPowerSeries.X(s) )^{e(s)}$$$
Lean4
theorem _root_.MvPowerSeries.prod_smul_X_eq_smul_monomial_one {A : Type*} [CommSemiring A] [Algebra A R] (e : σ →₀ ℕ)
(a : σ → A) :
e.prod (fun s n ↦ ((a s • MvPowerSeries.X s) ^ n)) =
(e.prod fun s n ↦ (a s) ^ n) • MvPowerSeries.monomial (R := R) e 1 :=
by
rw [Finsupp.prod_congr (g2 := fun s n ↦ ((MvPowerSeries.C (algebraMap A R (a s)) * (MvPowerSeries.X s)) ^ n))]
· have (a : A) (f : MvPowerSeries σ R) : a • f = MvPowerSeries.C ((algebraMap A R) a) * f := by
rw [← MvPowerSeries.smul_eq_C_mul, IsScalarTower.algebraMap_smul]
simp only [mul_pow, Finsupp.prod_mul, ← map_pow, ← MvPowerSeries.monomial_one_eq, this]
simp only [map_finsuppProd, map_pow]
· intro x _
rw [algebra_compatible_smul R, MvPowerSeries.smul_eq_C_mul]
