mathlib3

3fd7cc36 - 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.