chore: use order of power series to prove NoZeroDivisors (#24152)

This is the approach used in the multivariate case, and the current proof is essentially a hand-made version of the order argument.

This means moving all the results depending on this in a new file depending on `PowerSeries.Order`, which I call `PowerSeries.NoZeroDivisors` (analogous to the existing `MvPowerSeries.NoZeroDivisors`).

Also do a little bit of cleanup in the proof of `order_mul` using the cleanup from #24072.

This is a followup to #23993 and #24072.

Author: ADedecker

Mathlib.lean

@@ -5222,6 +5222,7 @@ import Mathlib.RingTheory.PowerSeries.Binomial
 import Mathlib.RingTheory.PowerSeries.Derivative
 import Mathlib.RingTheory.PowerSeries.Evaluation
 import Mathlib.RingTheory.PowerSeries.Inverse
+import Mathlib.RingTheory.PowerSeries.NoZeroDivisors
 import Mathlib.RingTheory.PowerSeries.Order
 import Mathlib.RingTheory.PowerSeries.PiTopology
 import Mathlib.RingTheory.PowerSeries.Trunc

Mathlib/RingTheory/DividedPowers/Basic.lean

@@ -7,6 +7,7 @@ Authors: Antoine Chambert-Loir, María-Inés de Frutos—Fernández
 import Mathlib.RingTheory.PowerSeries.Basic
 import Mathlib.Combinatorics.Enumerative.Bell
 import Mathlib.Data.Nat.Choose.Multinomial
+import Mathlib.RingTheory.Ideal.Maps
 
 /-! # Divided powers
 

Mathlib/RingTheory/PowerSeries/Basic.lean

@@ -6,10 +6,10 @@ Authors: Johan Commelin, Kenny Lau
 import Mathlib.Algebra.CharP.Defs
 import Mathlib.Algebra.Polynomial.AlgebraMap
 import Mathlib.Algebra.Polynomial.Basic
-import Mathlib.RingTheory.Ideal.Maps
 import Mathlib.RingTheory.MvPowerSeries.Basic
 import Mathlib.Tactic.MoveAdd
 import Mathlib.Algebra.MvPolynomial.Equiv
+import Mathlib.RingTheory.Ideal.Basic
 
 /-!
 # Formal power series (in one variable)
@@ -34,10 +34,6 @@ 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,
@@ -563,32 +559,6 @@ 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
@@ -764,45 +734,6 @@ theorem evalNegHom_X : evalNegHom (X : A⟦X⟧) = -X :=
 
 end CommRing
 
-section IsDomain
-
-instance [Ring R] [IsDomain R] : IsDomain R⟦X⟧ :=
-  NoZeroDivisors.to_isDomain _
-
-variable [CommRing R] [IsDomain R]
-
-/-- The ideal spanned by the variable in the power series ring
- over an integral domain is a prime ideal. -/
-theorem span_X_isPrime : (Ideal.span ({X} : Set R⟦X⟧)).IsPrime := by
-  suffices Ideal.span ({X} : Set R⟦X⟧) = RingHom.ker (constantCoeff R) by
-    rw [this]
-    exact RingHom.ker_isPrime _
-  apply Ideal.ext
-  intro φ
-  rw [RingHom.mem_ker, Ideal.mem_span_singleton, X_dvd_iff]
-
-/-- The variable of the power series ring over an integral domain is prime. -/
-theorem X_prime : Prime (X : R⟦X⟧) := by
-  rw [← Ideal.span_singleton_prime]
-  · exact span_X_isPrime
-  · intro h
-    simpa [map_zero (coeff R 1)] using congr_arg (coeff R 1) h
-
-/-- The variable of the power series ring over an integral domain is irreducible. -/
-theorem X_irreducible : Irreducible (X : R⟦X⟧) := X_prime.irreducible
-
-theorem rescale_injective {a : R} (ha : a ≠ 0) : Function.Injective (rescale a) := by
-  intro p q h
-  rw [PowerSeries.ext_iff] at *
-  intro n
-  specialize h n
-  rw [coeff_rescale, coeff_rescale, mul_eq_mul_left_iff] at h
-  apply h.resolve_right
-  intro h'
-  exact ha (pow_eq_zero h')
-
-end IsDomain
-
 section Algebra
 
 variable {A B : Type*} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B]

Mathlib/RingTheory/PowerSeries/Inverse.lean

@@ -7,8 +7,7 @@ Authors: Johan Commelin, Kenny Lau, María Inés de Frutos-Fernández, Filippo A
 import Mathlib.Algebra.Polynomial.FieldDivision
 import Mathlib.RingTheory.DiscreteValuationRing.Basic
 import Mathlib.RingTheory.MvPowerSeries.Inverse
-import Mathlib.RingTheory.PowerSeries.Basic
-import Mathlib.RingTheory.PowerSeries.Order
+import Mathlib.RingTheory.PowerSeries.NoZeroDivisors
 import Mathlib.RingTheory.LocalRing.ResidueField.Defs
 import Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
 import Mathlib.Data.ENat.Lattice

Mathlib/RingTheory/PowerSeries/NoZeroDivisors.lean

@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2019 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin, Kenny Lau
+-/
+import Mathlib.RingTheory.PowerSeries.Order
+import Mathlib.RingTheory.Ideal.Maps
+
+/-!
+# Power series over rings with no zero divisors
+
+This file proves, using the properties of orders of power series,
+that `R⟦X⟧` is an integral domain when `R` is.
+
+We then state various results about `R⟦X⟧` with `R` an integral domain.
+
+##  Instance
+
+If `R` has `NoZeroDivisors`, then so does `R⟦X⟧`.
+
+-/
+
+
+variable {R : Type*}
+
+namespace PowerSeries
+
+section NoZeroDivisors
+
+variable [Semiring R]
+
+instance [NoZeroDivisors R] : NoZeroDivisors R⟦X⟧ where
+  eq_zero_or_eq_zero_of_mul_eq_zero {φ ψ} h := by
+    simp_rw [← order_eq_top, order_mul] at h ⊢
+    exact WithTop.add_eq_top.mp h
+
+end NoZeroDivisors
+
+section IsDomain
+
+instance [Ring R] [IsDomain R] : IsDomain R⟦X⟧ :=
+  NoZeroDivisors.to_isDomain _
+
+variable [CommRing R] [IsDomain R]
+
+/-- The ideal spanned by the variable in the power series ring
+ over an integral domain is a prime ideal. -/
+theorem span_X_isPrime : (Ideal.span ({X} : Set R⟦X⟧)).IsPrime := by
+  suffices Ideal.span ({X} : Set R⟦X⟧) = RingHom.ker (constantCoeff R) by
+    rw [this]
+    exact RingHom.ker_isPrime _
+  apply Ideal.ext
+  intro φ
+  rw [RingHom.mem_ker, Ideal.mem_span_singleton, X_dvd_iff]
+
+/-- The variable of the power series ring over an integral domain is prime. -/
+theorem X_prime : Prime (X : R⟦X⟧) := by
+  rw [← Ideal.span_singleton_prime]
+  · exact span_X_isPrime
+  · intro h
+    simpa [map_zero (coeff R 1)] using congr_arg (coeff R 1) h
+
+/-- The variable of the power series ring over an integral domain is irreducible. -/
+theorem X_irreducible : Irreducible (X : R⟦X⟧) := X_prime.irreducible
+
+theorem rescale_injective {a : R} (ha : a ≠ 0) : Function.Injective (rescale a) := by
+  intro p q h
+  rw [PowerSeries.ext_iff] at *
+  intro n
+  specialize h n
+  rw [coeff_rescale, coeff_rescale, mul_eq_mul_left_iff] at h
+  apply h.resolve_right
+  intro h'
+  exact ha (pow_eq_zero h')
+
+end IsDomain
+
+end PowerSeries

Mathlib/RingTheory/PowerSeries/Order.lean

@@ -354,24 +354,18 @@ variable [Semiring R] [NoZeroDivisors R]
 is the sum of their orders. -/
 theorem order_mul (φ ψ : R⟦X⟧) : order (φ * ψ) = order φ + order ψ := by
   apply le_antisymm _ (le_order_mul _ _)
-  by_cases h : φ.order = ⊤ ∨ ψ.order = ⊤
+  by_cases h : φ = 0 ∨ ψ = 0
   · 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
+  · push_neg at h
+    rw [← coe_toNat_order h.1, ← coe_toNat_order h.2, ← ENat.coe_add]
     apply order_le
-    rw [coeff_mul, Finset.sum_eq_single ⟨m, n⟩]
-    · exact mul_ne_zero_iff.mpr ⟨hm.1, hn.1⟩
+    rw [coeff_mul, Finset.sum_eq_single_of_mem ⟨φ.order.toNat, ψ.order.toNat⟩ (by simp)]
+    · exact mul_ne_zero (coeff_order h.1) (coeff_order h.2)
     · 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]
+      · 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