if the dual of a well order is also a well order then finite

Stream: Is there code for X?

[Kenny Lau]

import data.fintype.basic

universe u

theorem fintype_of_well_order {α : Type u} (r : α → α → Prop)
  (H1 : is_well_order α r) (H2 : is_well_order α (flip r)) : fintype α :=
sorry

[Kenny Lau]

"if the dual of a well order is also a well order then the set is finite"

[Kenny Lau]

also what is the canonical way to write this

[Kenny Lau]

also the goal is to build the ring (or field) of functions with well-ordered support

[Kenny Lau]

the domain being a linearly ordered group

[Kevin Buzzard]

Are you doing this Hahn product thing?

[Kenny Lau]

oh so that's the name

[Kenny Lau]

https://en.wikipedia.org/wiki/Hahn_series

[Kevin Buzzard]

They're mentioned in Wedhorn's adic spaces notes

[Kevin Buzzard]

They play a role in the theory of valuations

[Kenny Lau]

so I assume it's already formalized in the perfectoid project?

[Kevin Buzzard]

No we didn't need them. We only formalised what we needed for perfectoid spaces

[Kevin Buzzard]

This is exactly the problem of formalising with an aim in mind