mathlib4
mathlib4 copied to clipboard
leanprover-community
Complete homogeneous and monomial symmetric polynomials
Implemented complete homogeneous symmetric functions. Request for comments. See also #10983.
Co-authored-by: Nirvana Coppola [email protected]
Ok, so, assuming that I'm good with this PR and want to start doing something else building up from here, what do I do? Do I keep working on this branch or is there another suggested procedure?
Ok, so, assuming that I'm good with this PR and want to start doing something else building up from here, what do I do? Do I keep working on this branch or is there another suggested procedure?
Probably the first thing is to make the build succeed :D
Uhm, okay, and how do I do that? Sorry, on my device everything seems to work, I'm confused about this.
It's a linting problem, not a build problem. You can write #lint at the end of the file and you will see the errors.
Ok now I'm confused. Commit 31ad0f7 was okay, but after merging the main branch into this one it doesn't work anymore?
This unfortunately happens all the time: a recent change in mathlib may have broken something in your code. I am having a look.
It is the fact that simp does not unfold let statement anymore (it is enough to add the name of what you want to unfold to the simp call). It should be fixed.
Implemented complete homogeneous symmetric functions. Request for comments. See also #10983.
Following the pull request convention, your PR description should use the present tense. Instead of writing Request for comments in the PR description, you can tag your PR with the RFC label. It's good to mention #10983 but, since this is not information relevant to the content of the PR but only to its review, you should put it under the --- in the PR description, so that it doesn't end up in mathlib's history forever (note this also applies to "Request for comments" or similar indications).
