feat(RingTheory): add HahnSeries.truncLT (#27055)

Author: wwylele

Mathlib/RingTheory/HahnSeries/Addition.lean

@@ -79,6 +79,9 @@ theorem le_order_smul {Γ} [Zero Γ] [LinearOrder Γ] (r : R) (x : HahnSeries Γ
     x.order ≤ (r • x).order :=
   le_of_not_gt (order_smul_not_lt r x h)
 
+theorem truncLT_smul [DecidableLT Γ] (c : Γ) (r : R) (x : HahnSeries Γ V) :
+    truncLT c (r • x) = r • truncLT c x := by ext; simp
+
 end SMulZeroClass
 
 section Addition
@@ -317,6 +320,11 @@ theorem embDomain_add (f : Γ ↪o Γ') (x y : HahnSeries Γ R) :
 
 end Domain
 
+theorem truncLT_add [DecidableLT Γ] (c : Γ) (x y : HahnSeries Γ R) :
+    truncLT c (x + y) = truncLT c x + truncLT c y := by
+  ext i
+  by_cases h : i < c <;> simp [h]
+
 end AddMonoid
 
 section AddCommMonoid
@@ -548,6 +556,18 @@ def embDomainLinearMap (f : Γ ↪o Γ') : HahnSeries Γ R →ₗ[R] HahnSeries
 
 end Domain
 
+variable (R) in
+/-- `HahnSeries.truncLT` as a linear map. -/
+def truncLTLinearMap [DecidableLT Γ] (c : Γ) : HahnSeries Γ V →ₗ[R] HahnSeries Γ V where
+  toFun := truncLT c
+  map_add' := truncLT_add c
+  map_smul' := truncLT_smul c
+
+variable (R) in
+@[simp]
+theorem coe_truncLTLinearMap [DecidableLT Γ] (c : Γ) :
+    (truncLTLinearMap R c : HahnSeries Γ V → HahnSeries Γ V) = truncLT c := by rfl
+
 end Module
 
 end HahnSeries

Mathlib/RingTheory/HahnSeries/Basic.lean

@@ -537,4 +537,31 @@ theorem order_ofForallLtEqZero [Zero Γ] (f : Γ → R) (hf : f ≠ 0) (n : Γ)
 
 end LocallyFiniteLinearOrder
 
+section Truncate
+variable [Zero R]
+
+/-- Zeroes out coefficients of a `HahnSeries` at indices not less than `c`. -/
+def truncLT [PartialOrder Γ] [DecidableLT Γ] (c : Γ) :
+    ZeroHom (HahnSeries Γ R) (HahnSeries Γ R) where
+  toFun x :=
+    { coeff i := if i < c then x.coeff i else 0
+      isPWO_support' := Set.IsPWO.mono x.isPWO_support (by simp) }
+  map_zero' := by ext; simp
+
+@[simp]
+protected theorem coeff_truncLT [PartialOrder Γ] [DecidableLT Γ]
+    (c : Γ) (x : HahnSeries Γ R) (i : Γ) :
+    (truncLT c x).coeff i = if i < c then x.coeff i else 0  := rfl
+
+theorem coeff_truncLT_of_lt [PartialOrder Γ] [DecidableLT Γ]
+    {c i : Γ} (h : i < c) (x : HahnSeries Γ R) : (truncLT c x).coeff i = x.coeff i := by
+  simp [h]
+
+theorem coeff_truncLT_of_le [LinearOrder Γ]
+    {c i : Γ} (h : c ≤ i) (x : HahnSeries Γ R) :
+    (truncLT c x).coeff i = 0 := by
+  simp [h]
+
+end Truncate
+
 end HahnSeries