Hahn embedding theorem

Stream: mathlib4

[Weiyi Wang]

Hi all, after learning Lean for a while, I decided to try some more serious project. I picked one of the unclaimed theorem from 1000+ theorem (somewhat randomly) and attempted to prove it. So here is the almost proved Hahn Embedding Theorem https://github.com/wwylele/HahnEmbedding. It still has one sorry that I think is trivial in theory but cumbersome to code (In Hahn.lean, the base case for zorn lemma, a linear map spanned by a family of disjoint submodules). I am trying to finish it this week.

My questions here are

• This is definitely not in mathlib yet, right? Do we want this in mathlib? (obviously not as-is. There are a lot of golfing to do)
• If we want this in mathlib, is it ok to make the codomain of the embedding HahnSeries like this code does? The original theorem simply specifies the codomain as "set of all functions from Ω to R which vanish outside a well-ordered set.". I used HahnSeries because it matches the definition and already has some useful API.

[Scott Carnahan]

Yes, HahnSeries is a good choice for codomain.

[Weiyi Wang]

:partying_face: It is sorry-less now. Time to clean up stuff and see if I can make this mathlib-ready

[Weiyi Wang]

I have started PR piece by piece in #25144