This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
[Merged by Bors] - feat(ring_theory/polynomial): show gaussian form of
hermite n
#18896[Merged by Bors] - feat(ring_theory/polynomial): show gaussian form of
hermite n
#18896Changes from 20 commits
c18d6fc
0139513
3eb686b
e3c4d85
44763e4
9d6e6ec
930aead
1ae19cf
22a9add
9fb7f4c
257a8f0
ed92185
0248c18
04fafe5
ac5025a
5ab5fb9
086953e
07044aa
e198737
c2e742f
3a28d9a
549d5d2
150bf46
a7b25eb
f3a41d2
98c4b9a
bdde511
e174f58
b6c1adc
a39abab
8c65b73
File filter
Filter by extension
Conversations
Jump to
There are no files selected for viewing
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 really want to add more to this PR at this point, but I should point out that there are 10-15 auxiliary lemmas here about
differentiable
and so on for(λx, p.eval x)
. Maybe some of these should be replicated foraeval
.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.
#18945
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.
These side goals go away if you work with
has_deriv_at
instead ofderiv
: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.
Actually also
deriv_const_mul_field
doesn't generate a side goal, I didn't notice it before (versusderiv_const_mul
).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.
The new version is pretty close to this, let's just go with it.