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 #7759

Closed
wants to merge 28 commits into from
Closed

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

wants to merge 28 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented May 30, 2021 •
edited

  • rename desc_fac to asc_factorial
  • define desc_factorial
  • update data.fintype.card_embedding to use desc_factorial

Open in Gitpod

@YaelDillies YaelDillies added the RFC Request for comment label May 30, 2021
@ericrbg
Copy link
Collaborator

ericrbg commented Jun 1, 2021

just an fyi: #7526 will be coming soon, with more merge conflicts. I'm happy to make them work (and probably change this + card_embedding to avoid nat subs) if you don't mind me pushing some stuff here

@YaelDillies
Copy link
Collaborator Author

Ah sure that's no problem. #7526 is probably gonna land before this PR, so I might just add here the few required. How do you want to get rid of nat substraction? I think it's pretty handy here, given that by the time nat substraction starts behaving "weird" you have already multiplied by 0 so you don't care.

@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jun 2, 2021
@ericrbg
Copy link
Collaborator

ericrbg commented Jun 2, 2021

The nat subtraction issues I meant in card_embedding and the other PR, as I think we both use the wrong factorial, leading to us using subs!

@YaelDillies
Copy link
Collaborator Author

Ah right! So I assume you mean using the correct one will solve those.

ericrbg
ericrbg reviewed Jun 3, 2021
View reviewed changes
src/data/nat/factorial.lean Outdated Show resolved Hide resolved
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jun 4, 2021
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR and removed RFC Request for comment labels Jun 4, 2021
@ericrbg
make some fintypes irreducible
4ec599e
@ericrbg
attributes :)
f17b1e1 
so we can't *remove* irreducible
but we *can* just locally add semireducible.
b-mehta
b-mehta reviewed Jun 9, 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
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
src/data/nat/choose/inequality.lean Outdated Show resolved Hide resolved
@b-mehta b-mehta removed the awaiting-review The author would like community review of the PR label Jun 10, 2021
@b-mehta b-mehta added the awaiting-author A reviewer has asked the author a question or requested changes label Jun 10, 2021
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 13, 2021
@YaelDillies YaelDillies changed the title feat(data/nat/factorial): descending factorial and exponential bounds on binomial coefficients feat(data/nat/factorial): descending factorial Jun 20, 2021
@YaelDillies
Copy link
Collaborator Author

I've now removed the new notations and inequalities. They will be follow up PRs. Could anyone review one last time? 🙂

@YaelDillies YaelDillies mentioned this pull request Jun 27, 2021
Closed
1 task
@b-mehta
Copy link
Collaborator

b-mehta commented Jun 27, 2021

Looks good to me, thanks!

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 Jun 27, 2021
bors bot pushed a commit that referenced this pull request Jun 27, 2021
@YaelDillies @ericrbg
feat(data/nat/factorial): descending factorial (#7759)
f8e9c17 
- rename `desc_fac` to `asc_factorial`
- define `desc_factorial`
- update `data.fintype.card_embedding` to use `desc_factorial`


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

bors bot commented Jun 27, 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 Jun 27, 2021
@bors bors bot closed this Jun 27, 2021
@bors bors bot deleted the asc_fac branch June 27, 2021 17:20
b-mehta pushed a commit that referenced this pull request Jul 6, 2021
@YaelDillies @ericrbg @b-mehta
feat(data/nat/factorial): descending factorial (#7759)
ea053bd 
- rename `desc_fac` to `asc_factorial`
- define `desc_factorial`
- update `data.fintype.card_embedding` to use `desc_factorial`


Co-authored-by: Eric <ericrboidi@gmail.com>
Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>
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

@fpvandoorn fpvandoorn fpvandoorn left review comments

@b-mehta b-mehta b-mehta left review comments

@ericrbg ericrbg ericrbg left review comments

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
@YaelDillies @ericrbg @b-mehta @eric-wieser @fpvandoorn