English
There is a ring homomorphism rescale(a) sending a multivariate series f to a new series whose n-th coefficient is multiplied by ∏ a(s)^m for s^m in n.
Русский
Существует кольцевой однозначный переход rescale(a), который отправляет f на новую серию, где коэффициент n умножается на произведение ∏ a(s)^{m_s} для разложения n.
LaTeX
$$$$\operatorname{rescale}(a)(f) = \sum_{n} \Bigl(\prod_{s} a(s)^{m_s}\Bigr) f_{n} X^{n},$$$$
Lean4
/-- The ring homomorphism taking a multivariate power series `f(X)` to `f(aX)`. -/
noncomputable def rescale (a : σ → R) : MvPowerSeries σ R →+* MvPowerSeries σ R
where
toFun f := fun n ↦ (n.prod fun s m ↦ a s ^ m) * f.coeff n
map_zero' := by
ext
simp [map_zero, coeff_apply]
map_one' := by
ext1 n
classical
simp only [coeff_one, mul_ite, mul_one, mul_zero]
split_ifs with h
· simp [h, coeff_apply]
· simp only [coeff_apply, ite_eq_right_iff]
exact fun a_1 ↦ False.elim (h a_1)
map_add' := by
intros
ext
exact mul_add _ _ _
map_mul' f
g := by
ext n
classical
rw [coeff_apply, coeff_mul, coeff_mul, Finset.mul_sum]
apply Finset.sum_congr rfl
intro x hx
simp only [Finset.mem_antidiagonal] at hx
rw [← hx]
simp only [coeff_apply]
rw [Finsupp.prod_of_support_subset _ Finsupp.support_add,
Finsupp.prod_of_support_subset x.1 Finset.subset_union_left,
Finsupp.prod_of_support_subset x.2 Finset.subset_union_right]
· simp only [← mul_assoc]
congr 1
rw [mul_assoc, mul_comm (f x.1), ← mul_assoc]
congr 1
rw [← Finset.prod_mul_distrib]
apply Finset.prod_congr rfl
simp [pow_add]
all_goals { simp
}
