feat (RingTheory/PowerSeries/Order) : compute order of power and generalize (#23993)

* compute order of power of power series
* generalize `order_mul`
* generalize lemmas at the end to `[Semiring R] [NoZeroDivisors R]` by proving (`PowerSeries.X_pow_mul_cancel`) that one can divide out by powers on `X` on both sides
of an equality.

Author: AntoineChambert-Loir

Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

@@ -314,6 +314,18 @@ end PartialOrder
 section LinearOrder
 variable [LinearOrder α] {a b c d : α}
 
+@[to_additive]
+theorem trichotomy_of_mul_eq_mul
+    [MulLeftStrictMono α] [MulRightStrictMono α]
+    (h : a * b = c * d) : (a = c ∧ b = d) ∨ a < c ∨ b < d := by
+  obtain hac | rfl | hca := lt_trichotomy a c
+  · right; left; exact hac
+  · left; simpa using mul_right_inj_of_comparable (LinearOrder.le_total d b)|>.1 h
+  · obtain hbd | rfl | hdb := lt_trichotomy b d
+    · right; right; exact hbd
+    · exact False.elim <| ne_of_lt (mul_lt_mul_right' hca b) h.symm
+    · exact False.elim <| ne_of_lt (mul_lt_mul_of_lt_of_lt hca hdb) h.symm
+
 @[to_additive]
 lemma mul_max [CovariantClass α α (· * ·) (· ≤ ·)] (a b c : α) :
     a * max b c = max (a * b) (a * c) := mul_left_mono.map_max

Mathlib/RingTheory/PowerSeries/Basic.lean

@@ -34,6 +34,10 @@ and the fact that power series over a local ring form a local ring;
 and application to the fact that power series over an integral domain
 form an integral domain.
 
+##  Instance
+
+If `R` has `NoZeroDivisors`, then so does `R⟦X⟧`.
+
 ## Implementation notes
 
 Because of its definition,
@@ -211,6 +215,9 @@ def X : R⟦X⟧ :=
 theorem commute_X (φ : R⟦X⟧) : Commute φ X :=
   MvPowerSeries.commute_X _ _
 
+theorem commute_X_pow (φ : R⟦X⟧) (n : ℕ) :
+    Commute φ (X ^ n) := Commute.pow_right (commute_X φ) n
+
 @[simp]
 theorem coeff_zero_eq_constantCoeff : ⇑(coeff R 0) = constantCoeff R := by
   rw [coeff, Finsupp.single_zero]
@@ -326,6 +333,22 @@ theorem coeff_succ_X_mul (n : ℕ) (φ : R⟦X⟧) : coeff R (n + 1) (X * φ) =
   convert φ.coeff_add_monomial_mul (single () 1) (single () n) _
   rw [one_mul]
 
+theorem mul_X_cancel {φ ψ : R⟦X⟧} (h : φ * X = ψ * X) : φ = ψ := by
+  rw [PowerSeries.ext_iff] at h ⊢
+  intro n
+  simpa using h (n + 1)
+
+theorem mul_X_inj {φ ψ : R⟦X⟧} : φ * X = ψ * X ↔ φ = ψ :=
+  ⟨mul_X_cancel, fun h ↦ congrFun (congrArg HMul.hMul h) X⟩
+
+theorem X_mul_cancel {φ ψ : R⟦X⟧} (h : X * φ = X * ψ) : φ = ψ := by
+  rw [PowerSeries.ext_iff] at h ⊢
+  intro n
+  simpa using h (n + 1)
+
+theorem X_mul_inj {φ ψ : R⟦X⟧} : X * φ = X * ψ ↔ φ = ψ :=
+  ⟨X_mul_cancel, fun h ↦ congrArg (HMul.hMul X) h⟩
+
 @[simp]
 theorem constantCoeff_C (a : R) : constantCoeff R (C R a) = a :=
   rfl
@@ -391,6 +414,26 @@ theorem coeff_X_pow_mul (p : R⟦X⟧) (n d : ℕ) :
   · rw [add_comm]
     exact fun h1 => (h1 (mem_antidiagonal.2 rfl)).elim
 
+theorem mul_X_pow_cancel {k : ℕ} {φ ψ : R⟦X⟧} (h : φ * X ^ k = ψ * X ^ k) :
+    φ = ψ := by
+  rw [PowerSeries.ext_iff] at h ⊢
+  intro n
+  simpa using h (n + k)
+
+theorem mul_X_pow_inj {k : ℕ} {φ ψ : R⟦X⟧} :
+      φ * X ^ k = ψ * X ^ k ↔ φ = ψ :=
+  ⟨mul_X_pow_cancel, fun h ↦ congrFun (congrArg HMul.hMul h) (X ^ k)⟩
+
+theorem X_pow_mul_cancel {k : ℕ} {φ ψ : R⟦X⟧} (h : X ^ k * φ = X ^ k * ψ) :
+    φ = ψ := by
+  rw [PowerSeries.ext_iff] at h ⊢
+  intro n
+  simpa using h (n + k)
+
+theorem X_mul_pow_inj {k : ℕ} {φ ψ : R⟦X⟧} :
+      X ^ k * φ = X ^ k * ψ ↔ φ = ψ :=
+  ⟨X_pow_mul_cancel, fun h ↦ congrArg (HMul.hMul (X ^ k)) h⟩
+
 theorem coeff_mul_X_pow' (p : R⟦X⟧) (n d : ℕ) :
     coeff R d (p * X ^ n) = ite (n ≤ d) (coeff R (d - n) p) 0 := by
   split_ifs with h
@@ -502,6 +545,32 @@ theorem X_dvd_iff {φ : R⟦X⟧} : (X : R⟦X⟧) ∣ φ ↔ constantCoeff R φ
   · intro m hm
     rwa [Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ hm)]
 
+instance [NoZeroDivisors R] : NoZeroDivisors R⟦X⟧ where
+  eq_zero_or_eq_zero_of_mul_eq_zero {φ ψ} h := by
+    classical
+    rw [or_iff_not_imp_left]
+    intro H
+    have ex : ∃ m, coeff R m φ ≠ 0 := by
+      contrapose! H
+      exact ext H
+    let m := Nat.find ex
+    ext n
+    rw [(coeff R n).map_zero]
+    induction' n using Nat.strong_induction_on with n ih
+    replace h := congr_arg (coeff R (m + n)) h
+    rw [LinearMap.map_zero, coeff_mul, Finset.sum_eq_single (m, n)] at h
+    · simp only [mul_eq_zero] at h
+      exact Or.resolve_left h (Nat.find_spec ex)
+    · rintro ⟨i, j⟩ hij hne
+      rw [mem_antidiagonal] at hij
+      rcases trichotomy_of_add_eq_add hij with h_eq | hi_lt | hj_lt
+      · apply False.elim (hne ?_)
+        simpa using h_eq
+      · suffices coeff R i φ = 0 by rw [this, zero_mul]
+        by_contra h; exact Nat.find_min ex hi_lt h
+      · rw [ih j hj_lt, mul_zero]
+    · simp
+
 end Semiring
 
 section CommSemiring
@@ -677,59 +746,11 @@ theorem evalNegHom_X : evalNegHom (X : A⟦X⟧) = -X :=
 
 end CommRing
 
-section Domain
-
-variable [Ring R]
-
-theorem eq_zero_or_eq_zero_of_mul_eq_zero [NoZeroDivisors R] (φ ψ : R⟦X⟧) (h : φ * ψ = 0) :
-    φ = 0 ∨ ψ = 0 := by
-  classical
-  rw [or_iff_not_imp_left]
-  intro H
-  have ex : ∃ m, coeff R m φ ≠ 0 := by
-    contrapose! H
-    exact ext H
-  let m := Nat.find ex
-  have hm₁ : coeff R m φ ≠ 0 := Nat.find_spec ex
-  have hm₂ : ∀ k < m, ¬coeff R k φ ≠ 0 := fun k => Nat.find_min ex
-  ext n
-  rw [(coeff R n).map_zero]
-  induction' n using Nat.strong_induction_on with n ih
-  replace h := congr_arg (coeff R (m + n)) h
-  rw [LinearMap.map_zero, coeff_mul, Finset.sum_eq_single (m, n)] at h
-  · replace h := NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero h
-    rw [or_iff_not_imp_left] at h
-    exact h hm₁
-  · rintro ⟨i, j⟩ hij hne
-    by_cases hj : j < n
-    · rw [ih j hj, mul_zero]
-    by_cases hi : i < m
-    · specialize hm₂ _ hi
-      push_neg at hm₂
-      rw [hm₂, zero_mul]
-    rw [mem_antidiagonal] at hij
-    push_neg at hi hj
-    suffices m < i by
-      have : m + n < i + j := add_lt_add_of_lt_of_le this hj
-      exfalso
-      exact ne_of_lt this hij.symm
-    contrapose! hne
-    obtain rfl := le_antisymm hi hne
-    simpa [Ne, Prod.mk_inj] using (add_right_inj m).mp hij
-  · contrapose!
-    intro
-    rw [mem_antidiagonal]
-
-instance [NoZeroDivisors R] : NoZeroDivisors R⟦X⟧ where
-  eq_zero_or_eq_zero_of_mul_eq_zero := eq_zero_or_eq_zero_of_mul_eq_zero _ _
+section IsDomain
 
-instance [IsDomain R] : IsDomain R⟦X⟧ :=
+instance [Ring R] [IsDomain R] : IsDomain R⟦X⟧ :=
   NoZeroDivisors.to_isDomain _
 
-end Domain
-
-section IsDomain
-
 variable [CommRing R] [IsDomain R]
 
 /-- The ideal spanned by the variable in the power series ring

Mathlib/RingTheory/PowerSeries/Order.lean

@@ -178,6 +178,14 @@ theorem le_order_mul (φ ψ : R⟦X⟧) : order φ + order ψ ≤ order (φ * ψ
   apply ne_of_lt (lt_of_lt_of_le hn <| add_le_add hi hj)
   rw [← Nat.cast_add, hij]
 
+theorem le_order_pow (φ : R⟦X⟧) (n : ℕ) : n • order φ ≤ order (φ ^ n) := by
+  induction n with
+  | zero => simp
+  | succ n hn =>
+    simp only [add_smul, one_smul, pow_succ]
+    apply le_trans _ (le_order_mul _ _)
+    exact add_le_add_right hn φ.order
+
 alias order_mul_ge := le_order_mul
 
 /-- The order of the monomial `a*X^n` is infinite if `a = 0` and `n` otherwise. -/
@@ -303,30 +311,58 @@ theorem order_X_pow (n : ℕ) : order ((X : R⟦X⟧) ^ n) = n := by
   rw [X_pow_eq, order_monomial_of_ne_zero]
   exact one_ne_zero
 
+@[simp]
+theorem divided_by_X_pow_order_of_X_eq_one :
+    divided_by_X_pow_order X_ne_zero = (1 : R⟦X⟧) := by
+  apply X_pow_mul_cancel
+  rw [self_eq_X_pow_order_mul_divided_by_X_pow_order]
+  simp
+
 end OrderZeroNeOne
 
-section OrderIsDomain
+section NoZeroDivisors
 
--- TODO: generalize to `[Semiring R] [NoZeroDivisors R]`
-variable [CommRing R] [IsDomain R]
+variable [Semiring R] [NoZeroDivisors R]
 
 /-- The order of the product of two formal power series over an integral domain
  is the sum of their orders. -/
 theorem order_mul (φ ψ : R⟦X⟧) : order (φ * ψ) = order φ + order ψ := by
-  classical
-  simp only [order_eq_emultiplicity_X]
-  exact emultiplicity_mul X_prime
-
--- Dividing `X` by the maximal power of `X` dividing it leaves `1`.
-@[simp]
-theorem divided_by_X_pow_order_of_X_eq_one : divided_by_X_pow_order X_ne_zero = (1 : R⟦X⟧) := by
-  rw [← mul_eq_left₀ X_ne_zero]
-  simpa using self_eq_X_pow_order_mul_divided_by_X_pow_order (@X_ne_zero R _ _)
+  apply le_antisymm _ (le_order_mul _ _)
+  by_cases h : φ.order = ⊤ ∨ ψ.order = ⊤
+  · rcases h with h | h <;> simp [h]
+  · simp only [not_or, ENat.ne_top_iff_exists] at h
+    obtain ⟨m, hm⟩ := h.1
+    obtain ⟨n, hn⟩ := h.2
+    rw [← hm, ← hn, ← ENat.coe_add]
+    rw [eq_comm, order_eq_nat] at hm hn
+    apply order_le
+    rw [coeff_mul, Finset.sum_eq_single ⟨m, n⟩]
+    · exact mul_ne_zero_iff.mpr ⟨hm.1, hn.1⟩
+    · intro ij hij h
+      rcases trichotomy_of_add_eq_add (mem_antidiagonal.mp hij) with h' | h' | h'
+      · exact False.elim (h (by simp [Prod.ext_iff, h'.1, h'.2]))
+      · rw [hm.2 ij.1 h', zero_mul]
+      · rw [hn.2 ij.2 h', mul_zero]
+    · intro h
+      apply False.elim (h _)
+      simp [mem_antidiagonal]
+
+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]
 
 -- Dividing a power series by the maximal power of `X` dividing it, respects multiplication.
 theorem divided_by_X_pow_orderMul {f g : R⟦X⟧} (hf : f ≠ 0) (hg : g ≠ 0) :
     divided_by_X_pow_order hf * divided_by_X_pow_order hg =
-      divided_by_X_pow_order (mul_ne_zero hf hg) := by
+      divided_by_X_pow_order ((mul_ne_zero_iff_right hg).mpr hf) := by
   set df := f.order.lift (order_finite_iff_ne_zero.mpr hf)
   set dg := g.order.lift (order_finite_iff_ne_zero.mpr hg)
   set dfg := (f * g).order.lift (order_finite_iff_ne_zero.mpr (mul_ne_zero hf hg))
@@ -338,15 +374,16 @@ theorem divided_by_X_pow_orderMul {f g : R⟦X⟧} (hf : f ≠ 0) (hg : g ≠ 0)
       f * g = X ^ df * divided_by_X_pow_order hf * (X ^ dg * divided_by_X_pow_order hg) := by
         rw [self_eq_X_pow_order_mul_divided_by_X_pow_order,
           self_eq_X_pow_order_mul_divided_by_X_pow_order]
-      _ = X ^ df * X ^ dg * divided_by_X_pow_order hf * divided_by_X_pow_order hg := by ring
+      _ = X ^ df * X ^ dg * divided_by_X_pow_order hf * divided_by_X_pow_order hg := by
+        rw [mul_assoc, ← mul_assoc _ (X ^ dg), (commute_iff_eq _ _).mp (commute_X_pow _ _)];
+        simp [mul_assoc]
       _ = X ^ (df + dg) * divided_by_X_pow_order hf * divided_by_X_pow_order hg := by rw [pow_add]
       _ = X ^ dfg * divided_by_X_pow_order hf * divided_by_X_pow_order hg := by rw [H_add_d]
       _ = X ^ dfg * (divided_by_X_pow_order hf * divided_by_X_pow_order hg) := by rw [mul_assoc]
-  refine (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero (pow_ne_zero dfg X_ne_zero) ?_).symm
-  simp only [this] at H
-  convert H
+  apply X_pow_mul_cancel
+  rw [← this, H]
 
-end OrderIsDomain
+end NoZeroDivisors
 
 end PowerSeries