Ordering on Hahn series

Stream: mathlib4

[Violeta Hernández]

#25168 added a LinearOrder instance on docs#HahnSeries. Might I ask why it's defined on the Lex type and not directly? I don't believe there is any other reasonable ordering one might give Hahn series. The colex ordering doesn't work, since the value group is only well-founded in one direction. The pointwise ordering does work, but isn't mathematically interesting. @Weiyi Wang @Eric Wieser

[Violeta Hernández]

FTR, the lexicographic ordering is the one that gives the isomorphism between surreals and real Hahn series over themselves.

[Eric Wieser]

This was discussed in the PR here

[Eric Wieser]

This was partly just me saying "deciding whether to make this the order is bikeshedding, let's not let the rest to go waste in the meantime"

[Violeta Hernández]

Hm, I think I see the reasoning. Putting global orders on other power series structures would be odd, so we don't do it here either

[Eric Wieser]

Odd enough that it made sense to wait for someone to complain that Lex was inconvenient

[Violeta Hernández]

Well... I guess I'll have to actually try it out and see how much I can hide it.