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
feat(ring_theory/polynomial): more operations on polynomials #679
Conversation
693b3c7
to
c7584ae
Compare
f623d34
to
1ed7ad1
Compare
c7584ae
to
3289836
Compare
⟨p.support, subtype.val ∘ p.to_fun, | ||
λ n, finsupp.mem_support_iff.trans (not_iff_not_of_iff | ||
⟨λ h, congr_arg subtype.val h, λ h, subtype.eq h⟩)⟩ | ||
|
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.
This is just map subtype.val
, I don't think it needs to be defined again.
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.
This has better definitional equalities.
|
||
@[simp] theorem monic_restriction {p : polynomial R} : monic (restriction p) ↔ monic p := | ||
⟨λ H, congr_arg subtype.val H, λ H, subtype.eq H⟩ | ||
|
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.
Does ⟨congr_arg subtype.val, subtype.eq⟩
work here.
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.
I don't think it would work: congr_arg
is very stubborn.
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list