New user, planning to do some homological algebra

Stream: new members

[Liran Shaul]

Hi, I am Liran Shaul, an homological algebraist from Prague. I have some plans to try to add some major results in Homological algebra to Lean. As a small test, I just added to the injective module file in matlab a result showing that direct product of injectives is injective. I think I was able to push this to the github, but it was not yet approved. I am not sure if I need to do anything for it to be approved.

[Bryan Gin-ge Chen]

Welcome! Looks like your PR is at #31263 and is waiting for CI to finish seeing if the code compiles and passes linting, etc. You probably have already seen it but our guide for contributors is here and describes the contribution flow in some detail.

[Liran Shaul]

Bryan Gin-ge Chen said:

Welcome! Looks like your PR is at #31263 and is waiting for CI to finish seeing if the code compiles and passes linting, etc. You probably have already seen it but our guide for contributors is here and describes the contribution flow in some detail.

Thank you! I did not see this before. It is helpful.

[Axel Boldt]

It seems that in the rest of Injective.lean, they consider slightly more general situations where the ring R can belong to any universe, not just to Type like in your addition. Also, they seem to have certain naming conventions for their theorems which you aren't following. Maybe that's why the pull request is held up.

[Liran Shaul]

I hope someone could help me. I accepted some suggestions for imporvements, but after accepting one of them, it stopped compiling. I tried to revert back to last known version, but it still seem to suggest an error on github, despite working earlier. Can anyone take a look? thank you.

[Michael Rothgang]

I can take a look at your PR and give you some style feedback; hopefully tomorrow.

[Andrew Yang]

Have you tried to open the file locally? It should tell you the error.