Commit 2025-09-14 09:24 0c276458

feat(Algebra/Order): Hahn embedding theorem, part 1 (#27043) Part 1 of Hahn embedding theorem, or the core part of it. This proves that one can embed an ordered module in HahnSeries. To obtain the full Hahn embedding theorem, one needs to specialize the coefficient of HahnSeries to Real as a module over Rat, and compose with another embedding from ordered group to ordered module. These will be in part 2 There is a debatable design here: throughout the file, all lemmas uses an input HahnEmbedding.Seed. Because the the final theorem is an existence theorem without specifying what HahnEmbedding.Seed is used, it is possible to Classical.choose a seed from the very beginning (provided R = Real ), and the entire file will just use the same chosen seed. Overall, choosing everything from the beginning will likely make the code a little bit more concise. I decided against choosing anything till the final step, for the reason that such choice is not canonical for an arbitrary module, and there may be future use of this construction with more canonical choice for specific modules. Examples are:

• if the input is a HahnSeries Γ R, the canonical choice for the stratum would be HahnSeries.single
• for the field version of Hahn embedding theorem ("every linearly ordered field can be embedded in HahnSeries as a field", not implemented), the canonical choice should ensure that all stratum form a graded ring, and the coeff should map (1 : M) to (1 : R). But if the argument is not strong enough, I am OK with converting everything to a classical choose.