feat(RingTheory/PowerSeries/Substitution): add API

Mathlib/RingTheory/PowerSeries/Basic.lean

@@ -624,6 +624,18 @@ theorem rescale_mul (a b : R) : rescale (a * b) = (rescale b).comp (rescale a) :
   ext
   simp [← rescale_rescale]
 
+theorem rescale_map_eq_map_rescale' {S : Type*} [CommSemiring S] (φ : R →+* S) (r : R) (f : R⟦X⟧) :
+    rescale (φ r) (PowerSeries.map φ f) =
+      PowerSeries.map (φ : R →+* S) (rescale r f) := by
+  ext n
+  simp [coeff_rescale, coeff_map, map_mul, map_pow]
+
+theorem rescale_map_eq_map_rescale {A S : Type*} [CommSemiring A] [Algebra A R] [CommSemiring S]
+    [Algebra A S] (φ : R →ₐ[A] S) (a : A) (f : R⟦X⟧) :
+    rescale (algebraMap A S a) (PowerSeries.map φ f) =
+      PowerSeries.map (φ : R →+* S) (rescale (algebraMap A R a) f) := by
+  rw [← rescale_map_eq_map_rescale', RingHom.coe_coe, AlgHom.commutes]
+
 end CommSemiring
 
 section CommSemiring

Mathlib/RingTheory/PowerSeries/Substitution.lean

@@ -3,7 +3,7 @@ Copyright (c) 2025 Antoine Chambert-Loir, María Inés de Frutos Fernández. All
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Antoine Chambert-Loir, María Inés de Frutos Fernández
 -/
-
+import Mathlib.RingTheory.MvPowerSeries.Order
 import Mathlib.RingTheory.MvPowerSeries.Substitution
 import Mathlib.RingTheory.PowerSeries.Evaluation
 
@@ -146,6 +146,9 @@ noncomputable def subst (a : MvPowerSeries τ S) (f : PowerSeries R) :
     MvPowerSeries τ S :=
   MvPowerSeries.subst (fun _ ↦ a) f
 
+lemma subst_def (a : MvPowerSeries τ S) (f : PowerSeries R) :
+    subst a f = MvPowerSeries.subst (fun _ ↦ a) f := rfl
+
 variable {a : MvPowerSeries τ S} {b : S⟦X⟧}
 
 /-- Substitution of power series into a power series, as an `AlgHom`. -/
@@ -284,10 +287,57 @@ theorem subst_comp_subst_apply
     subst b (subst a f) = subst (subst b a) f :=
   congr_fun (subst_comp_subst ha hb) f
 
+lemma rescale_eq (r : R) (f : PowerSeries R) :
+    rescale r f = MvPowerSeries.rescale (fun _ ↦ r) f := by
+  ext n
+  rw [coeff_rescale, coeff, MvPowerSeries.coeff_rescale]
+  simp [pow_zero, Finsupp.prod_single_index]
+
+lemma rescale_eq_subst (r : R) (f : PowerSeries R) :
+    PowerSeries.rescale r f = PowerSeries.subst (r • X : R⟦X⟧) f := by
+  rw [rescale_eq, MvPowerSeries.rescale_eq_subst, X, subst, Pi.smul_def']
+
 theorem _root_.MvPowerSeries.rescaleUnit (a : R) (f : R⟦X⟧) :
     MvPowerSeries.rescale (Function.const _ a) f = rescale a f := by
   ext d
   rw [coeff_rescale, coeff, MvPowerSeries.coeff_rescale]
   simp
 
+/-- Rescale power series, as an `AlgHom` -/
+noncomputable def rescaleAlgHom (r : R) : R⟦X⟧ →ₐ[R] R⟦X⟧ :=
+  MvPowerSeries.rescaleAlgHom (fun _ ↦ r)
+
+lemma rescaleAlgHom_def (r : R) (f : PowerSeries R) :
+    rescaleAlgHom r f = MvPowerSeries.rescaleAlgHom (fun _ ↦ r) f := by
+  simp only [rescaleAlgHom]
+
+theorem rescaleAlgHom_apply (r : R) :
+    (rescaleAlgHom r) = rescale r := by
+  ext f
+  rw [rescale_eq, RingHom.coe_coe, rescaleAlgHom_def, MvPowerSeries.rescaleAlgHom_apply]
+
+/-- When `p` is linear, substitution of `p` and then a scalar homothety is substitution of
+  the homothety then `p`. -/
+lemma subst_linear_subst_scalar_comm (a : R) {σ : Type*} (p : MvPowerSeries σ R)
+    (hp_lin : ∀ d ∈ Function.support p, d.degree = 1) (f : PowerSeries R) :
+    subst p (rescale a f) = MvPowerSeries.rescale (Function.const σ a) (subst p f) := by
+  have hp : PowerSeries.HasSubst p := by
+    apply HasSubst.of_constantCoeff_zero
+    rw [← MvPowerSeries.coeff_zero_eq_constantCoeff_apply]
+    apply MvPowerSeries.IsHomogeneous.coeff_eq_zero (p := 1) _ (by simp)
+    simp only [MvPowerSeries.IsHomogeneous, MvPowerSeries.IsWeightedHomogeneous, ne_eq]
+    intro d hd
+    convert hp_lin d hd using 1
+    simp [Finsupp.weight, Finsupp.linearCombination, Finsupp.degree]
+    rfl
+  rw [rescale_eq_subst, MvPowerSeries.rescale_eq_subst,
+    subst_comp_subst_apply (HasSubst.smul_X' a) hp]
+  nth_rewrite 3 [subst]
+  rw [MvPowerSeries.subst_comp_subst_apply hp.const (MvPowerSeries.HasSubst.smul_X _),
+    funext_iff]
+  intro _
+  rw [subst_smul hp, ← Polynomial.coe_X, subst_coe hp, Polynomial.aeval_X,
+    ← MvPowerSeries.rescale_eq_subst, MvPowerSeries.rescale_homogeneous_eq_smul hp_lin,
+    subst, pow_one]
+
 end PowerSeries