rescale_homogeneous_eq_smul — Mathlib

English

Rescaling by a and then substituting is the same as substituting by a X and then applying rescale.

Русский

Масштабирование по a затем подстановка эквивалентны подстановке по a·X затем масштабированию.

LaTeX

$$$\operatorname{rescale}(a) f = \operatorname{subst}(a \cdot X) f$$$

Lean4

/-- Rescaling a homogeneous power series -/
theorem rescale_homogeneous_eq_smul {n : ℕ} {r : R} {f : MvPowerSeries σ R} (hf : ∀ d ∈ f.support, d.degree = n) :
    MvPowerSeries.rescale (Function.const σ r) f = r ^ n • f :=
  by
  ext e
  simp only [MvPowerSeries.coeff_rescale, map_smul, Finsupp.prod, Function.const_apply, Finset.prod_pow_eq_pow_sum,
    smul_eq_mul]
  by_cases he : e ∈ f.support
  · rw [← hf e he, Finsupp.degree]
  · simp only [Function.mem_support, ne_eq, not_not] at he
    simp [he, mul_zero, coeff_apply]

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