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/list/big_operators): More lemmas about alternating product #13195

Closed
wants to merge 11 commits into from
Closed

[Merged by Bors] - feat(data/list/big_operators): More lemmas about alternating product #13195

wants to merge 11 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Apr 6, 2022 •
edited

A few more lemmas about list.alternating_prod and list.alternating_sum and a proof that 11 divides even length base 10 palindromes.

Also rename palindrome to list.palindrome (as it should have been).

Co-authored-by: Chris Wong

Open in Gitpod

@YaelDillies YaelDillies added the awaiting-review The author would like community review of the PR label Apr 6, 2022
@eric-wieser
Copy link
Member

This moves palindrome to list.palindrome, right? The PR description doesn't mention that!

@YaelDillies
Copy link
Collaborator Author

Whoops! Done now.

@urkud
Copy link
Member

urkud commented Apr 8, 2022

Also, I'm not sure that Co-Authored-By works without an e-mail (never tried). But bors add authors of all commits anyway, right? Otherwise, LGTM.
bors d+

@bors
Copy link

bors bot commented Apr 8, 2022

✌️ YaelDillies 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 Apr 8, 2022
@eric-wieser
Copy link
Member

This should probably be rebased so that the first commit is Yaël's, else bors will mixed up author names and emails.

Yury is correct about Co-authored-by

@Vierkantor
Copy link
Collaborator

I did the rebase, apparently Git now recorded me as committer (and Chris/Yaël as author). I hope that's fine, let me know if you want me to rebase again while impersonating someone else :)

@YaelDillies
Copy link
Collaborator Author

bors merge

bors bot pushed a commit that referenced this pull request Apr 9, 2022
@YaelDillies @lambda-fairy
feat(data/list/big_operators): More lemmas about alternating product (#…
2a04ec0 
…13195)

A few more lemmas about `list.alternating_prod` and `list.alternating_sum` and a proof that 11 divides even length base 10 palindromes.

Also rename `palindrome` to `list.palindrome` (as it should have been).

Co-authored-by: Chris Wong



Co-authored-by: Chris Wong <lambda.fairy@gmail.com>
@bors
Copy link

bors bot commented Apr 9, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/list/big_operators): More lemmas about alternating product [Merged by Bors] - feat(data/list/big_operators): More lemmas about alternating product Apr 9, 2022
@bors bors bot closed this Apr 9, 2022
@bors bors bot deleted the dvd_11 branch April 9, 2022 01:53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@YaelDillies @eric-wieser @urkud @Vierkantor @lambda-fairy