Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(data/polynomial/hasse_deriv): Hasse derivatives #8998

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat(data/polynomial/hasse_deriv): Hasse derivatives #8998

wants to merge 12 commits into from

Conversation

jcommelin
Copy link
Member

@jcommelin jcommelin commented Sep 4, 2021 •
edited by github-actions bot
Loading

@jcommelin
feat(data/nat/choose/vandermonde): Vandermonde's identity for binomia…
70332e0 
…l coefficients

I place this identity in a new file because the current proof depends on `polynomial`.
@jcommelin
feat(data/polynomial/hasse_deriv): Hasse derivatives
f357acc
@jcommelin jcommelin added awaiting-review The author would like community review of the PR blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Sep 4, 2021
@jcommelin jcommelin mentioned this pull request Sep 4, 2021
Closed
2 tasks
@github-actions github-actions bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Sep 6, 2021
@github-actions
Copy link

github-actions bot commented Sep 6, 2021

🎉 Great news! Looks like all the dependencies have been resolved:

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

jcommelin and others added 2 commits September 6, 2021 13:13
@jcommelin @eric-wieser
Apply suggestions from code review
2a5875a 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@jcommelin
Revert "Apply suggestions from code review"
d9a676d 
This reverts commit 2a5875a.
semorrison
semorrison reviewed Sep 7, 2021
View reviewed changes
src/data/polynomial/hasse_deriv.lean
have h2 : k ≤ i - l := nat.le_sub_right_of_add_le hikl,
have h3 : k ≤ k + l := le_self_add,
have H : ∀ (n : ℕ), (n! : ℚ) ≠ 0, { exact_mod_cast factorial_ne_zero },
-- why can't `field_simp` help me here?
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What are you wanting it to do here? Perhaps explain or remove?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Given H, it should be able to remove all the divisions from the goal state. But it doesn't.

@jcommelin @semorrison
Apply suggestions from code review
d383281 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@semorrison
Copy link
Collaborator

bors d+

@bors
Copy link

bors bot commented Sep 7, 2021

✌️ jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Sep 7, 2021
@jcommelin
Copy link
Member Author

Thanks 🎉

bors merge

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Sep 8, 2021
bors bot pushed a commit that referenced this pull request Sep 8, 2021
@jcommelin
feat(data/polynomial/hasse_deriv): Hasse derivatives (#8998)
56a59d3
@bors
Copy link

bors bot commented Sep 8, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/polynomial/hasse_deriv): Hasse derivatives [Merged by Bors] - feat(data/polynomial/hasse_deriv): Hasse derivatives Sep 8, 2021
@bors bors bot closed this Sep 8, 2021
@bors bors bot deleted the hasse-deriv branch September 8, 2021 19:07
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@semorrison semorrison semorrison left review comments

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@jcommelin @semorrison @eric-wieser