submodule of free module over PID is free

Stream: condensed mathematics

[Fabian Glöckle]

There is now a sorry-free proof of the "submodules of free modules over PIDs are free" statement (arbitrary rank). It is pretty slow and convoluted and needs lots of clean-up work before going into mathlib.
But @Riccardo Brasca mentioned to me that at the moment you do not aim for elegance. Do you prefer the "ugly" version right now, or should I already do some cleanup beforehand?

[Johan Commelin]

Feel free to push it to for_mathlib/ in the LTE repo, and cleanup afterwards.

[Johan Commelin]

@Fabian Glöckle What is your github username?

[Fabian Glöckle]

faabian (2 'a', no typo)

[Johan Commelin]

https://github.com/leanprover-community/lean-liquid/invitations

[Johan Commelin]

Congrats on getting this sorry-free!

[Kevin Buzzard]

Just to remark that @Pierre-Alexandre Bazin is well on the way to proving the structure theorem for fg modules over a PID

[Riccardo Brasca]

Congratulations!