Commit 2021-05-10 22:45 3fd7cc36

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.