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(algebra/group/basic): reduce additivity checks to one case #18080

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - feat(algebra/group/basic): reduce additivity checks to one case #18080

wants to merge 6 commits into from

Conversation

alreadydone
Copy link
Collaborator

@alreadydone alreadydone commented Jan 7, 2023 •
edited

Can be used to reduce lemmas like interval_integral.integral_add_adjacent_intervals to one case. Intended to be used in #18040.

ported in leanprover-community/mathlib4#1519
an earlier version ported in leanprover-community/mathlib4#1399

Open in Gitpod

@alreadydone alreadydone added awaiting-review The author would like community review of the PR modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. labels Jan 7, 2023
@alreadydone alreadydone mentioned this pull request Jan 7, 2023
Closed
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jan 7, 2023
@alreadydone
feat: synchronize with mathlib3 #18080 (#1399)
c2b7c75 
matches leanprover-community/mathlib#18080
@bottine bottine mentioned this pull request Jan 9, 2023
Closed
1 task
@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jan 12, 2023
@alreadydone alreadydone 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 Jan 12, 2023
@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jan 12, 2023
@alreadydone alreadydone 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 Jan 12, 2023
@sgouezel
Copy link
Collaborator

bors r+
Don't forget to port to mathlib4!

@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 Jan 13, 2023
@alreadydone
Copy link
Collaborator Author

Thanks! The mathlib4 PR was already merged, but I'll update the SHA after this is merged.

bors bot pushed a commit that referenced this pull request Jan 13, 2023
@alreadydone
feat(algebra/group/basic): reduce additivity checks to one case (#18080)
685660e 
Can be used to reduce lemmas like [interval_integral.integral_add_adjacent_intervals](https://leanprover-community.github.io/mathlib_docs/measure_theory/integral/interval_integral.html#interval_integral.integral_add_adjacent_intervals) to one case. Intended to be used in [#18040](#18040 (comment)).
@bors
Copy link

bors bot commented Jan 13, 2023

This PR was included in a batch that was canceled, it will be automatically retried

bors bot pushed a commit that referenced this pull request Jan 13, 2023
@alreadydone
feat(algebra/group/basic): reduce additivity checks to one case (#18080)
bb5963c 
Can be used to reduce lemmas like [interval_integral.integral_add_adjacent_intervals](https://leanprover-community.github.io/mathlib_docs/measure_theory/integral/interval_integral.html#interval_integral.integral_add_adjacent_intervals) to one case. Intended to be used in [#18040](#18040 (comment)).
@bors
Copy link

bors bot commented Jan 13, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Jan 13, 2023
@alreadydone
feat(algebra/group/basic): reduce additivity checks to one case (#18080)
c5b83bd 
Can be used to reduce lemmas like [interval_integral.integral_add_adjacent_intervals](https://leanprover-community.github.io/mathlib_docs/measure_theory/integral/interval_integral.html#interval_integral.integral_add_adjacent_intervals) to one case. Intended to be used in [#18040](#18040 (comment)).
@bors
Copy link

bors bot commented Jan 13, 2023

Build failed (retrying...):

urkud
urkud reviewed Jan 13, 2023
View reviewed changes
src/algebra/group/basic.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented Jan 13, 2023

Canceled.

@urkud
Copy link
Member

urkud commented Jan 13, 2023 •
edited

Fixed a typo. Also, this lemma is not useful for interval_integral.integral_add_adjacent_intervals because it doesn't deal with an extra predicate (interval_integrable). Could you please either generalize it and use in interval_integral.integral_add_adjacent_intervals or drop this statement from the commit message?
bors r-

urkud
urkud reviewed Jan 13, 2023
View reviewed changes
src/algebra/group/basic.lean Outdated Show resolved Hide resolved
@alreadydone alreadydone mentioned this pull request Jan 14, 2023
Closed
3 tasks
@alreadydone alreadydone added awaiting-review The author would like community review of the PR and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Jan 14, 2023
@alreadydone
Copy link
Collaborator Author

@sgouezel @urkud Can we merge this if there's no more comment? Thanks!

@urkud
Copy link
Member

urkud commented Jan 19, 2023

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 Jan 19, 2023
bors bot pushed a commit that referenced this pull request Jan 19, 2023
@alreadydone @urkud
feat(algebra/group/basic): reduce additivity checks to one case (#18080)
4060545 
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@bors
Copy link

bors bot commented Jan 19, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra/group/basic): reduce additivity checks to one case [Merged by Bors] - feat(algebra/group/basic): reduce additivity checks to one case Jan 19, 2023
@bors bors bot closed this Jan 19, 2023
@bors bors bot deleted the multiplicative_of_total branch January 19, 2023 21:39
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jan 25, 2023
@alreadydone
feat: synchronize with mathlib3#18080/18160/18174 (#1519)
48c2c12 
- [x] leanprover-community/mathlib#18080
- [x] leanprover-community/mathlib#18160
- [ ] leanprover-community/mathlib#18174



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
@j-loreaux j-loreaux mentioned this pull request Jun 19, 2023
Closed
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jun 20, 2023
@urkud @j-loreaux
feat: port Analysis.BoundedVariation (#4824)
0817363 
This PR also corrects a mis-forward-port of leanprover-community/mathlib#18080



Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
alexkeizer pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jun 22, 2023
@urkud @j-loreaux @alexkeizer
feat: port Analysis.BoundedVariation (#4824)
cf40008 
This PR also corrects a mis-forward-port of leanprover-community/mathlib#18080



Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
semorrison pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jun 23, 2023
@urkud @j-loreaux @semorrison
feat: port Analysis.BoundedVariation (#4824)
2e1353d 
This PR also corrects a mis-forward-port of leanprover-community/mathlib#18080



Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
semorrison pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jun 23, 2023
@urkud @j-loreaux @semorrison
feat: port Analysis.BoundedVariation (#4824)
25c8f65 
This PR also corrects a mis-forward-port of leanprover-community/mathlib#18080



Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
semorrison pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jun 25, 2023
@urkud @j-loreaux @semorrison
feat: port Analysis.BoundedVariation (#4824)
42cf029 
This PR also corrects a mis-forward-port of leanprover-community/mathlib#18080



Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
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

@sgouezel sgouezel sgouezel left review comments

Assignees
No one assigned
Labels
modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. 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
3 participants
@alreadydone @sgouezel @urkud