Working on flat modules

Stream: new members

[Wojtek Wawrów]

I am planning to start some work on some basic results about flat modules (first goal would be establishing equivalence to some standard definitions). However I'm a little unsure how to set it up. The proofs I would be doing would ideally eventually end up in ring_theory/flat.lean file. I don't think messing with that file directly in mathlib folder is a good idea. Should I copy that file to src and work from there? Or should I just create a blank file, import ring_theory.flat and whatever else and work from there?

[Wojtek Wawrów]

Also a soft question, beyond the guidelines as listed here https://leanprover-community.github.io/contribute/index.html is there anything I shoukd keep in mind when working on my first project? :)

[Kevin Buzzard]

You should clone mathlib locally, make a new branch (this is the key point, and what git enables you do to) and then sure, go ahead and mess directly with that file!

[Johan Commelin]

@Wojtek Wawrów That's a brave plan! As mentioned in flat.lean, I think that https://stacks.math.columbia.edu/tag/00HD should be one of the first goals.

[Johan Commelin]

But beware that this is not a Lean-triviality.

[Wojtek Wawrów]

I have created a new branch (I hope), but then I think I broke something - I got some popup about leanpkg, I pressed it, and now the Lean Infoview is stuck on "Loading..." without any errors/warnings or anything

[Kevin Buzzard]

@Wojtek Wawrów if you want to hop over to the discord I can try and help you fix things.

[Wojtek Wawrów]

Crisis averted!