feat(RingTheory/PowerSeries/Order): PowerSeries.divXPowOrder_pow (#31331)

* Deprecate `divXPowOrder_mul_divXPowerOrder` in favour of `divXPowOrder_mul` (the same equality in reverse, the conventional direction for monoid homs)
* Define MonoidHom versions of `order` and `divXPowOrder` and use them to prove `order_pow` and `order_prod`, `divXPowOrder_pow` and `divXPowOrder_prod` (in a nontrivial semiring with no zero divisors).

Author: bustercopley

Mathlib/RingTheory/PowerSeries/Inverse.lean

@@ -327,7 +327,7 @@ instance : NormalizationMonoid k⟦X⟧ where
     simp only [← mul_inv, inv_inj]
     simp only [Unit_of_divided_by_X_pow_order_nonzero (mul_ne_zero hf hg),
       Unit_of_divided_by_X_pow_order_nonzero hf, Unit_of_divided_by_X_pow_order_nonzero hg,
-      Units.ext_iff, Units.val_mul, divXPowOrder_mul_divXPowOrder]
+      Units.ext_iff, Units.val_mul, ← divXPowOrder_mul]
   normUnit_coe_units := by
     intro u
     set u₀ := u.1 with hu

Mathlib/RingTheory/PowerSeries/Order.lean

@@ -346,6 +346,10 @@ theorem divXPowOrder_X :
   ext n
   simp [coeff_X]
 
+theorem divXPowOrder_one : divXPowOrder 1 = (1 : R⟦X⟧) := by
+  ext k
+  simp
+
 end OrderZeroNeOne
 
 section NoZeroDivisors
@@ -369,44 +373,64 @@ theorem order_mul (φ ψ : R⟦X⟧) : order (φ * ψ) = order φ + order ψ :=
       · rw [coeff_of_lt_order_toNat ij.1 h', zero_mul]
       · rw [coeff_of_lt_order_toNat ij.2 h', mul_zero]
 
-theorem order_pow [Nontrivial R] (φ : R⟦X⟧) (n : ℕ) :
-    order (φ ^ n) = n • order φ := by
-  rcases subsingleton_or_nontrivial R with hR | hR
-  · simp only [Subsingleton.eq_zero φ, order_zero, nsmul_eq_mul]
-    by_cases hn : n = 0
-    · simp [hn, pow_zero]
-    · simp [zero_pow hn, ENat.mul_top', if_neg hn]
-  induction n with
-  | zero => simp
-  | succ n hn =>
-    simp only [add_smul, one_smul, pow_succ, order_mul, hn]
-
-theorem order_prod {R : Type*} [CommSemiring R] [NoZeroDivisors R] [Nontrivial R] {ι : Type*}
-    (φ : ι → R⟦X⟧) (s : Finset ι) : (∏ i ∈ s, φ i).order = ∑ i ∈ s, (φ i).order := by
-  induction s using Finset.cons_induction with
-  | empty => simp
-  | cons a s ha ih => rw [Finset.sum_cons ha, Finset.prod_cons ha, order_mul, ih]
-
 /-- The operation of dividing a power series by the largest possible power of `X`
 preserves multiplication. -/
-theorem divXPowOrder_mul_divXPowOrder {f g : R⟦X⟧} :
-    divXPowOrder f * divXPowOrder g = divXPowOrder (f * g) := by
+theorem divXPowOrder_mul {f g : R⟦X⟧} :
+    divXPowOrder (f * g) = divXPowOrder f * divXPowOrder g := by
   by_cases h : f = 0 ∨ g = 0
   · rcases h with (h | h) <;> simp [h]
   push_neg at h
   apply X_pow_mul_cancel (k := f.order.toNat + g.order.toNat)
   calc
-    X ^ (f.order.toNat + g.order.toNat) * (f.divXPowOrder * g.divXPowOrder)
-    _ = (X ^ f.order.toNat * f.divXPowOrder) * (X ^ g.order.toNat * g.divXPowOrder) := by
-        conv_rhs =>
-          rw [mul_assoc, X_pow_mul, X_pow_mul, ← mul_assoc, mul_assoc, ← pow_add]
-        rw [X_pow_mul, add_comm]
+    _ = X ^ ((f * g).order.toNat) * (f * g).divXPowOrder := by
+        rw [order_mul, ENat.toNat_add (order_eq_top.not.mpr h.1) (order_eq_top.not.mpr h.2)]
     _ = f * g := by
         simp [X_pow_order_mul_divXPowOrder]
-    _ = X ^ ((f * g).order.toNat) * (f * g).divXPowOrder := by
+    _ = (X ^ f.order.toNat * f.divXPowOrder) * (X ^ g.order.toNat * g.divXPowOrder) := by
         simp [X_pow_order_mul_divXPowOrder]
-    _ = X ^ (f.order.toNat + g.order.toNat) * (f * g).divXPowOrder := by
-        rw [order_mul, ENat.toNat_add (order_eq_top.not.mpr h.1) (order_eq_top.not.mpr h.2)]
+    _ = f.divXPowOrder * g.divXPowOrder * X ^ (g.order.toNat + f.order.toNat) := by
+        rw [mul_assoc, X_pow_mul, X_pow_mul, ← mul_assoc, mul_assoc, ← pow_add]
+    _ = X ^ (f.order.toNat + g.order.toNat) * (f.divXPowOrder * g.divXPowOrder) := by
+        rw [X_pow_mul, add_comm]
+
+@[deprecated divXPowOrder_mul "use `divXPowOrder_mul.symm` instead" (since := "2025-11-06")]
+theorem divXPowOrder_mul_divXPowOrder {f g : R⟦X⟧} :
+    divXPowOrder f * divXPowOrder g = divXPowOrder (f * g) :=
+  divXPowOrder_mul.symm
+
+variable [Nontrivial R]
+
+/-- `PowerSeries.order` as a `MonoidHom`. -/
+def orderHom : R⟦X⟧ →* Multiplicative ℕ∞ where
+  toFun g := .ofAdd g.order
+  map_one' := order_one
+  map_mul' := order_mul
+
+@[simp, norm_cast]
+lemma coe_orderHom : (orderHom : R⟦X⟧ → ℕ∞) = order := rfl
+
+theorem order_pow (φ : R⟦X⟧) (n : ℕ) : order (φ ^ n) = n • order φ :=
+  map_pow orderHom φ n
+
+theorem order_prod {R : Type*} [CommSemiring R] [NoZeroDivisors R] [Nontrivial R] {ι : Type*}
+    (φ : ι → R⟦X⟧) (s : Finset ι) : (∏ i ∈ s, φ i).order = ∑ i ∈ s, (φ i).order :=
+  map_prod orderHom φ s
+
+/-- `PowerSeries.divXPowOrder` as a `MonoidHom`. -/
+def divXPowOrderHom : R⟦X⟧ →* R⟦X⟧ where
+  toFun g := g.divXPowOrder
+  map_one' := divXPowOrder_one
+  map_mul' f g := divXPowOrder_mul (f := f) (g := g)
+
+@[simp, norm_cast]
+lemma coe_divXPowOrderHom : (divXPowOrderHom : R⟦X⟧ → R⟦X⟧) = divXPowOrder := rfl
+
+theorem divXPowOrder_pow (φ : R⟦X⟧) (n : ℕ) : divXPowOrder (φ ^ n) = (divXPowOrder φ) ^ n :=
+  map_pow divXPowOrderHom φ n
+
+theorem divXPowOrder_prod {R : Type*} [CommSemiring R] [NoZeroDivisors R] [Nontrivial R] {ι : Type*}
+    (φ : ι → R⟦X⟧) (s : Finset ι) : (∏ i ∈ s, φ i).divXPowOrder = ∏ i ∈ s, (φ i).divXPowOrder :=
+  map_prod divXPowOrderHom φ s
 
 end NoZeroDivisors