feat(RingTheory): add HahnSeries.ofFinsupp (leanprover-community#28136)

Part of leanprover-community#27043 Hahn's embedding theorem

Author: wwylele

Mathlib/RingTheory/HahnSeries/Addition.lean

@@ -6,6 +6,7 @@ Authors: Aaron Anderson
 import Mathlib.Algebra.Group.Support
 import Mathlib.Algebra.Module.Basic
 import Mathlib.Algebra.Module.LinearMap.Defs
+import Mathlib.Data.Finsupp.SMul
 import Mathlib.RingTheory.HahnSeries.Basic
 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 import Mathlib.Tactic.FastInstance
@@ -507,6 +508,26 @@ protected lemma map_smul [AddCommMonoid U] [Module R U] (f : U →ₗ[R] V) {r :
     {x : HahnSeries Γ U} : (r • x).map f = r • ((x.map f) : HahnSeries Γ V) := by
   ext; simp
 
+section Finsupp
+
+variable (R) in
+/-- `ofFinsupp` as a linear map. -/
+def ofFinsuppLinearMap : (Γ →₀ V) →ₗ[R] HahnSeries Γ V where
+  toFun := ofFinsupp
+  map_add' _ _ := by
+    ext
+    simp
+  map_smul' _ _ := by
+    ext
+    simp
+
+variable (R) in
+@[simp]
+theorem coeff_ofFinsuppLinearMap (f : Γ →₀ V) (a : Γ) :
+    (ofFinsuppLinearMap R f).coeff a = f a := rfl
+
+end Finsupp
+
 section Domain
 
 variable [PartialOrder Γ']

Mathlib/RingTheory/HahnSeries/Basic.lean

@@ -5,6 +5,7 @@ Authors: Aaron Anderson
 -/
 import Mathlib.Algebra.Notation.Support
 import Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
+import Mathlib.Data.Finsupp.Defs
 import Mathlib.Order.WellFoundedSet
 
 /-!
@@ -405,6 +406,18 @@ theorem leadingCoeff_eq {x : HahnSeries Γ R} : x.leadingCoeff = x.coeff x.order
 
 end Order
 
+section Finsupp
+
+/-- Create a `HahnSeries` with a `Finsupp` as coefficients. -/
+def ofFinsupp : ZeroHom (Γ →₀ R) (HahnSeries Γ R) where
+  toFun f := { coeff := f, isPWO_support' := f.finite_support.isPWO }
+  map_zero' := by simp
+
+@[simp]
+theorem coeff_ofFinsupp (f : Γ →₀ R) (a : Γ) : (ofFinsupp f).coeff a = f a := rfl
+
+end Finsupp
+
 section Domain
 
 variable [PartialOrder Γ']