feat(ring_theory/hahn_series): extend the domain of a Hahn series by an `order_embedding` (#7551)
feat(ring_theory/hahn_series): extend the domain of a Hahn series by an `order_embedding` (#7551)

Defines `hahn_series.emb_domain`, which extends the domain of a Hahn series by embedding it into a larger domain in an order-preserving way.
Bundles `hahn_series.emb_domain` with additional properties as `emb_domain_linear_map`, `emb_domain_ring_hom`, and `emb_domain_alg_hom` under additional conditions.
Defines the ring homomorphism `hahn_series.of_power_series` and the algebra homomorphism `hahn_series.of_power_series_alg`, which map power series to Hahn series over an ordered semiring using `hahn_series.emb_domain` with `nat.cast` as the embedding.





leanprover-community/mathlib,leanprover-community/mathlib