monomial_smul_const — Mathlib

English

A scalar multiple form of the monomial identity: monomial e with r^{sum n} equals product of (r•X_s)^{e(s)}.

Русский

Умножение мономиала на константу: monomial e с коэффициентом r^{sum e(s)} равен произведению (r·X_s)^{e(s)}.

LaTeX

$$$\\mathrm{MvPowerSeries.monomial}(e, r^{\\sum e}) = \\prod_s ( r \\,\\mathrm{MvPowerSeries.X}(s) )^{e(s)}$$$

Lean4

theorem _root_.MvPowerSeries.monomial_smul_const {σ : Type*} {R : Type*} [CommSemiring R] (e : σ →₀ ℕ) (r : R) :
    MvPowerSeries.monomial e (r ^ (e.sum fun _ n => n)) = (e.prod fun s e => (r • MvPowerSeries.X s) ^ e) :=
  by
  rw [MvPowerSeries.prod_smul_X_eq_smul_monomial_one, ← map_smul, smul_eq_mul, mul_one]
  simp only [Finsupp.sum, Finsupp.prod, Finset.prod_pow_eq_pow_sum]

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