Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(data/nat/factorial) : descending factorial #7527

Closed
wants to merge 24 commits into from
Closed

[Merged by Bors] - feat(data/nat/factorial) : descending factorial #7527

wants to merge 24 commits into from

Conversation

ericrbg
Copy link
Collaborator

@ericrbg ericrbg commented May 6, 2021

Essentially pochhammer, but for nat. Used in #7363 and #7526.

Open in Gitpod

This was referenced May 6, 2021
Closed
Closed
ericrbg and others added 2 commits May 6, 2021 10:42
@ericrbg @benjamindavidson
golf
e96129b 
Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>
@ericrbg
golf right
b071cb2
@ericrbg ericrbg added the awaiting-review The author would like community review of the PR label May 6, 2021
@jcommelin jcommelin requested a review from semorrison May 6, 2021 13:30
@ericrbg
Copy link
Collaborator Author

ericrbg commented May 8, 2021

Alright, actually, before I do it all (sorry, got caught up today!), let me think what's best:

  • pochhammer doesn't have any nat specialized lemmas, apart from saying that pochhammer nat = desc_fac. This probably makes generalizing slightly harder than the current simpa using congr_arg proofs, but it feels like it "fits" more.
  • bernstein's aux gets moved out into pochhammer and desc_fac.
  • I make desc_fac feature equal to pochhmamer.

Does this seem good to everyone?

ericrbg
ericrbg commented May 9, 2021
View reviewed changes
src/data/nat/factorial.lean Outdated Show resolved Hide resolved
@ericrbg @benjamindavidson
ac_refl begone
652ea0d 
Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>
ericrbg and others added 2 commits May 10, 2021 10:25
@ericrbg @jcommelin
Update src/data/nat/factorial.lean
f60504c 
Co-authored-by: Johan Commelin <johan@commelin.net>
@ericrbg
avoid 100-char linter
cb6ce9b
benjamindavidson
benjamindavidson reviewed May 10, 2021
View reviewed changes
src/data/nat/factorial.lean Outdated Show resolved Hide resolved
src/data/nat/factorial.lean Outdated Show resolved Hide resolved
src/data/nat/factorial.lean Outdated Show resolved Hide resolved
ericrbg and others added 3 commits May 10, 2021 11:39
benjamindavidson
benjamindavidson reviewed May 11, 2021
View reviewed changes
Copy link
Collaborator

@benjamindavidson benjamindavidson left a comment

Choose a reason for hiding this comment

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

A couple of minor comments, otherwise LGTM.

src/ring_theory/polynomial/bernstein.lean Outdated Show resolved Hide resolved
src/ring_theory/polynomial/bernstein.lean Outdated Show resolved Hide resolved
ericrbg and others added 2 commits May 11, 2021 10:39
@ericrbg
use rw_mod_cast
455ca4f
@ericrbg @benjamindavidson
more rw_mod_cast and stop rwing away succ
90f0f6b 
I'm in a bad habit with that because of `ring` not dealing with `succ` well...

Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>
ericrbg and others added 2 commits May 11, 2021 10:55
@ericrbg @eric-wieser
improve readability
5f5dfaf 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@ericrbg @eric-wieser
split eval_succ
58d855e 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@semorrison
Copy link
Collaborator

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels May 15, 2021
bors bot pushed a commit that referenced this pull request May 15, 2021
@ericrbg
feat(data/nat/factorial) : descending factorial (#7527)
94aae73 


Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>
@bors
Copy link

bors bot commented May 15, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/nat/factorial) : descending factorial [Merged by Bors] - feat(data/nat/factorial) : descending factorial May 15, 2021
@bors bors bot closed this May 15, 2021
@bors bors bot deleted the desc_fac branch May 15, 2021 08:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

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

@jcommelin jcommelin jcommelin left review comments

@benjamindavidson benjamindavidson benjamindavidson left review comments

@semorrison semorrison Awaiting requested review from semorrison

Assignees
No one assigned
Labels
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.

None yet
5 participants
@ericrbg @semorrison @eric-wieser @jcommelin @benjamindavidson