feat: cardinality of Hahn series inverse (leanprover-community#32643)

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: 2 people

Mathlib/RingTheory/HahnSeries/Addition.lean

@@ -267,16 +267,12 @@ theorem order_lt_order_of_eq_add_single {R} {Γ} [LinearOrder Γ] [Zero Γ] [Add
     exact hyne rfl
   refine lt_of_le_of_ne ?_ this
   simp only [order, ne_zero_of_eq_add_single hxy hy, ↓reduceDIte, hy]
-  have : y.support ⊆ x.support := by
-    intro g hg
-    by_cases hgx : g = x.order
-    · refine (mem_support x g).mpr ?_
-      have : x.coeff x.order ≠ 0 := coeff_order_ne_zero <| ne_zero_of_eq_add_single hxy hy
-      rwa [← hgx] at this
-    · have : x.coeff g = (y + (single x.order) x.leadingCoeff).coeff g := by rw [← hxy]
-      rw [coeff_add, coeff_single_of_ne hgx, add_zero] at this
-      simpa [this] using hg
-  exact Set.IsWF.min_le_min_of_subset this
+  refine Set.IsWF.min_le_min_of_subset fun g hg ↦ ?_
+  obtain rfl | hgx := eq_or_ne g x.order
+  · simpa using coeff_order_eq_zero.not.2 <| ne_zero_of_eq_add_single hxy hy
+  · have : x.coeff g = (y + (single x.order) x.leadingCoeff).coeff g := by rw [← hxy]
+    rw [coeff_add, coeff_single_of_ne hgx, add_zero] at this
+    simpa [this] using hg
 
 /-- `single` as an additive monoid/group homomorphism -/
 @[simps!]

Mathlib/RingTheory/HahnSeries/Basic.lean

@@ -384,10 +384,16 @@ theorem order_eq_orderTop_of_ne_zero (hx : x ≠ 0) : order x = orderTop x := by
 
 @[deprecated (since := "2025-08-19")] alias order_eq_orderTop_of_ne := order_eq_orderTop_of_ne_zero
 
-theorem coeff_order_ne_zero {x : R⟦Γ⟧} (hx : x ≠ 0) : x.coeff x.order ≠ 0 := by
+@[simp]
+theorem coeff_order_eq_zero {x : R⟦Γ⟧} : x.coeff x.order = 0 ↔ x = 0 := by
+  refine ⟨not_imp_not.1 fun hx ↦ ?_, by simp +contextual⟩
   rw [order_of_ne hx]
   exact x.isWF_support.min_mem (support_nonempty_iff.2 hx)
 
+@[deprecated coeff_order_eq_zero (since := "2025-12-09")]
+theorem coeff_order_ne_zero {x : R⟦Γ⟧} (hx : x ≠ 0) : x.coeff x.order ≠ 0 :=
+  coeff_order_eq_zero.not.2 hx
+
 theorem order_le_of_coeff_ne_zero {Γ} [Zero Γ] [LinearOrder Γ] {x : R⟦Γ⟧}
     {g : Γ} (h : x.coeff g ≠ 0) : x.order ≤ g :=
   le_trans (le_of_eq (order_of_ne (ne_zero_of_coeff_ne_zero h)))

Mathlib/RingTheory/HahnSeries/Cardinal.lean

@@ -5,8 +5,10 @@ Authors: Violeta Hernández Palacios
 -/
 module
 
-public import Mathlib.Algebra.Group.Pointwise.Set.Card
-public import Mathlib.RingTheory.HahnSeries.Multiplication
+public import Mathlib.RingTheory.HahnSeries.Summable
+public import Mathlib.SetTheory.Cardinal.Arithmetic
+
+import Mathlib.Algebra.Group.Pointwise.Set.Card
 
 /-!
 # Cardinality of Hahn series
@@ -16,7 +18,6 @@ for the cardinalities of different operations.
 
 ## Todo
 
-- Bound the cardinality of the inverse.
 - Build the subgroups, subrings, etc. of Hahn series with support less than a given infinite
   cardinal.
 -/
@@ -27,10 +28,13 @@ open Cardinal
 
 namespace HahnSeries
 
-variable {Γ R S : Type*} [PartialOrder Γ]
+variable {Γ R S α : Type*}
 
 /-! ### Cardinality function -/
 
+section PartialOrder
+variable [PartialOrder Γ]
+
 section Zero
 variable [Zero R]
 
@@ -56,6 +60,14 @@ theorem cardSupp_single_of_ne (a : Γ) {r : R} (h : r ≠ 0) : cardSupp (single
 theorem cardSupp_single_le (a : Γ) (r : R) : cardSupp (single a r) ≤ 1 :=
   (mk_le_mk_of_subset support_single_subset).trans_eq (mk_singleton a)
 
+@[simp]
+theorem cardSupp_one_le [Zero Γ] [One R] : cardSupp (1 : R⟦Γ⟧) ≤ 1 :=
+  cardSupp_single_le ..
+
+@[simp]
+theorem cardSupp_one [Zero Γ] [One R] [NeZero (1 : R)] : cardSupp (1 : R⟦Γ⟧) = 1 :=
+  cardSupp_single_of_ne _ one_ne_zero
+
 theorem cardSupp_map_le [Zero S] (x : R⟦Γ⟧) (f : ZeroHom R S) : (x.map f).cardSupp ≤ x.cardSupp :=
   cardSupp_mono <| support_map_subset ..
 
@@ -85,4 +97,53 @@ theorem cardSupp_mul_le [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [NonUni
     (x y : R⟦Γ⟧) : (x * y).cardSupp ≤ x.cardSupp * y.cardSupp :=
   (mk_le_mk_of_subset (support_mul_subset ..)).trans mk_add_le
 
+theorem cardSupp_single_mul_le [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ]
+    [NonUnitalNonAssocSemiring R] (x : R⟦Γ⟧) (a : Γ) (r : R) :
+    (single a r * x).cardSupp ≤ x.cardSupp := by
+  simpa using (cardSupp_mul_le ..).trans (mul_le_mul_left (cardSupp_single_le ..) _)
+
+theorem cardSupp_mul_single_le [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ]
+    [NonUnitalNonAssocSemiring R] (x : R⟦Γ⟧) (a : Γ) (r : R) :
+    (x * single a r).cardSupp ≤ x.cardSupp := by
+  simpa using (cardSupp_mul_le ..).trans (mul_le_mul_right (cardSupp_single_le ..) _)
+
+theorem cardSupp_pow_le [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R]
+    (x : R⟦Γ⟧) (n : ℕ) : (x ^ n).cardSupp ≤ x.cardSupp ^ n := by
+  induction n with
+  | zero => simp
+  | succ n IH =>
+    simpa [pow_succ] using (cardSupp_mul_le ..).trans <| mul_le_mul_left IH _
+
+theorem cardSupp_hsum_le [AddCommMonoid R] (s : SummableFamily Γ R α) :
+    lift s.hsum.cardSupp ≤ sum fun a ↦ (s a).cardSupp :=
+  (lift_le.2 <| mk_le_mk_of_subset (SummableFamily.support_hsum_subset ..)).trans
+    mk_iUnion_le_sum_mk_lift
+
+end PartialOrder
+
+section LinearOrder
+variable [LinearOrder Γ]
+
+theorem cardSupp_hsum_powers_le [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R]
+    (x : R⟦Γ⟧) : (SummableFamily.powers x).hsum.cardSupp ≤ max ℵ₀ x.cardSupp := by
+  grw [← lift_uzero (cardSupp _), ← sum_pow_le_max_aleph0, cardSupp_hsum_le, sum_le_sum]
+  intro i
+  rw [SummableFamily.powers_toFun]
+  split_ifs
+  · exact cardSupp_pow_le ..
+  · cases i <;> simp
+
+theorem cardSupp_inv_le [AddCommGroup Γ] [IsOrderedAddMonoid Γ] [Field R] (x : R⟦Γ⟧) :
+    x⁻¹.cardSupp ≤ max ℵ₀ x.cardSupp := by
+  obtain rfl | hx := eq_or_ne x 0; · simp
+  apply (cardSupp_single_mul_le ..).trans <| (cardSupp_hsum_powers_le ..).trans _
+  gcongr
+  refine (cardSupp_single_mul_le _ (-x.order) x.leadingCoeff⁻¹).trans' <| cardSupp_mono fun _ ↦ ?_
+  aesop (add simp [coeff_single_mul])
+
+theorem cardSupp_div_le [AddCommGroup Γ] [IsOrderedAddMonoid Γ] [Field R] (x y : R⟦Γ⟧) :
+    (x / y).cardSupp ≤ x.cardSupp * max ℵ₀ y.cardSupp :=
+  (cardSupp_mul_le ..).trans <| mul_le_mul_right (cardSupp_inv_le y) _
+
+end LinearOrder
 end HahnSeries

Mathlib/RingTheory/HahnSeries/Multiplication.lean

@@ -473,6 +473,16 @@ theorem coeff_mul_single_add [NonUnitalNonAssocSemiring R] {r : R} {x : R⟦Γ
       simp [hx]
   · simp
 
+theorem coeff_single_mul [NonUnitalNonAssocSemiring R] [PartialOrder Γ'] [AddCommGroup Γ']
+    [IsOrderedAddMonoid Γ'] {r : R} {x : R⟦Γ'⟧} {a b : Γ'} :
+    (single b r * x).coeff a = r * x.coeff (a - b) := by
+  simpa using coeff_single_mul_add (a := a - b) (b := b)
+
+theorem coeff_mul_single [NonUnitalNonAssocSemiring R] [PartialOrder Γ'] [AddCommGroup Γ']
+    [IsOrderedAddMonoid Γ'] {r : R} {x : R⟦Γ'⟧} {a b : Γ'} :
+    (x * single b r).coeff a = x.coeff (a - b) * r := by
+  simpa using coeff_mul_single_add (a := a - b) (b := b)
+
 @[simp]
 theorem coeff_mul_single_zero [NonUnitalNonAssocSemiring R] {r : R} {x : R⟦Γ⟧} {a : Γ} :
     (x * single 0 r).coeff a = x.coeff a * r := by rw [← add_zero a, coeff_mul_single_add, add_zero]

Mathlib/RingTheory/LaurentSeries.lean

@@ -226,8 +226,8 @@ theorem powerSeriesPart_eq_zero (x : R⸨X⸩) : x.powerSeriesPart = 0 ↔ x = 0
     simp only [ne_eq]
     intro h
     rw [PowerSeries.ext_iff, not_forall]
-    refine ⟨0, ?_⟩
-    simp [coeff_order_ne_zero h]
+    use 0
+    simpa
   · rintro rfl
     simp