-
Notifications
You must be signed in to change notification settings - Fork 299
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(ring_theory/polynomial/homogeneous): definition and basic props #3223
Conversation
This PR also move ring_theory/polynomial.lean to ring_theory/polynomial/basic.lean This PR is part of bringing symmetric polynomials to mathlib, and besided that, I also expect to add binomial polynomials and Chebyshev polynomials in the future. Altogether, this motivates the starting of a ring_theory/polynomial directory. The file basic.lean may need cleaning or splitting at some point.
…_theory.polynomial.basic` This PR is the intersection of #3223 and #3241, allowing them to be merged in either order. Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/where.20should.20these.20definitions.20live.3F
…_theory.polynomial.basic` (#3248) This PR is the intersection of #3223 and #3241, allowing them to be merged in either order. Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/where.20should.20these.20definitions.20live.3F Co-authored-by: Johan Commelin <johan@commelin.net>
import data.mv_polynomial | ||
import data.fintype.card | ||
import tactic | ||
#print tactic.interactive.squeeze_simp |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
#print tactic.interactive.squeeze_simp |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why did this pass CI? @bryangingechen @robertylewis
I remember putting this #print
statement here exactly because I wanted CI to remind me that I should minimize imports... but apparently that trick doesn't work.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
CI doesn't check for a lack of #print
statements. If you want a warning, #check
a declaration that doesn't exist.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ooh, I thought it would complain about printing output...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It should be possible to set it up to do that. I can't work on it right now, but please make an issue if you think it's a feature worth having and I'll try to come back to it when I can.
LGTM otherwise. bors d+ |
✌️ jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
No idea why the docs build failed, but I see this is on an old Lean, so I'm gonna merge master. |
bors merge |
…3223) This PR also move ring_theory/polynomial.lean to ring_theory/polynomial/basic.lean This PR is part of bringing symmetric polynomials to mathlib, and besided that, I also expect to add binomial polynomials and Chebyshev polynomials in the future. Altogether, this motivates the starting of a ring_theory/polynomial directory. The file basic.lean may need cleaning or splitting at some point. Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Pull request successfully merged into master. Build succeeded: |
…_theory.polynomial.basic` (leanprover-community#3248) This PR is the intersection of leanprover-community#3223 and leanprover-community#3241, allowing them to be merged in either order. Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/where.20should.20these.20definitions.20live.3F Co-authored-by: Johan Commelin <johan@commelin.net>
This PR also move ring_theory/polynomial.lean to
ring_theory/polynomial/basic.lean
This PR is part of bringing symmetric polynomials to mathlib,
and besided that, I also expect to add binomial polynomials
and Chebyshev polynomials in the future.
Altogether, this motivates the starting of a ring_theory/polynomial
directory.
The file basic.lean may need cleaning or splitting at some point.