## Stream: Is there code for X?

### Topic: if the dual of a well order is also a well order then finite

#### Kenny Lau (Jun 11 2020 at 06:45):

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 (Jun 11 2020 at 06:46):

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

#### Kenny Lau (Jun 11 2020 at 06:49):

also what is the canonical way to write this

#### Kenny Lau (Jun 11 2020 at 06:49):

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

#### Kenny Lau (Jun 11 2020 at 06:54):

the domain being a linearly ordered group

#### Kevin Buzzard (Jun 11 2020 at 07:35):

Are you doing this Hahn product thing?

#### Kenny Lau (Jun 11 2020 at 07:45):

oh so that's the name

#### Kenny Lau (Jun 11 2020 at 07:45):

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

#### Kevin Buzzard (Jun 11 2020 at 07:49):

They're mentioned in Wedhorn's adic spaces notes

#### Kevin Buzzard (Jun 11 2020 at 07:49):

They play a role in the theory of valuations

#### Kenny Lau (Jun 11 2020 at 07:50):

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

#### Kevin Buzzard (Jun 11 2020 at 08:06):

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

#### Kevin Buzzard (Jun 11 2020 at 08:06):

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

Last updated: May 16 2021 at 05:21 UTC