HahnSeries.orderTop

Stream: mathlib4

[Violeta Hernández]

Can anyone guess what docs#HahnSeries.orderTop is (or what its output type is) without looking?

[Violeta Hernández]

I hope it's not controversial to suggest this should be renamed to degree instead.

[Violeta Hernández]

Ohh wait, I just noticed. It's called orderTop not because of docs#OrderTop but rather because it's a version of docs#HahnSeries.order with a top.

[Yaël Dillies]

Yes, the name is very weird. And no it's not the degree either!

[Yaël Dillies]

I would rather have order/finOrder rather than orderTop/order

[Violeta Hernández]

I like that suggestion

[Violeta Hernández]

@Weiyi Wang since I think he's the Hahn series guy

[Yakov Pechersky]

"trailingDegree". But also, order makes sense from the valuation point of view.

[Weiyi Wang]

Renaming HahnSeries.orderTop to HahnSeries.order would make it more consistent with PowerSeries.order

[Yakov Pechersky]

And existing order can be natOrder a la natDegree

[Weiyi Wang]

But HahnSeries' order is not necessarily a Nat. It is any PartialOrder type

[Yakov Pechersky]

Do we need the not top version? Can users rely on untop instead?

[Yaël Dillies]

The not-top version is useful just as docs#Polynomial.natDegree is useful: Sometimes you want to use it as an exponent, and junk values align to make unified statements including the zero polynomial

[Scott Carnahan]

Sorry about the orderTop name. HahnSeries.order had been around for years by the time I found that I needed a version that didn’t assume the presence of a Zero. Yaël’s suggestion of order/finOrder seems good to me.