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: add lemmas about Sum #1583

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - Feat: add lemmas about Sum #1583

wants to merge 3 commits into from

Conversation

urkud
Copy link
Member

@urkud urkud commented Jan 16, 2023

This is the Lean 4 version of leanprover-community/mathlib#18184

Open in Gitpod

@urkud urkud added awaiting-review The author would like community review of the PR mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged labels Jan 16, 2023
@urkud urkud mentioned this pull request Jan 16, 2023
Closed
bors bot pushed a commit to leanprover-community/mathlib that referenced this pull request Jan 16, 2023
@urkud
feat(data/sum/basic): add some missing lemmas (#18184)
f4ecb59 
Forward-ported to Mathlib 4 in leanprover-community/mathlib4#1583
kbuzzard
kbuzzard approved these changes Jan 18, 2023
View reviewed changes
Copy link
Member

@kbuzzard kbuzzard left a comment

Choose a reason for hiding this comment

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

LGTM! I think the convention with #align nowadays is no blank line beforehand.

Mathlib/Data/Sum/Basic.lean Outdated Show resolved Hide resolved
Mathlib/Data/Sum/Basic.lean Outdated Show resolved Hide resolved
@urkud @kbuzzard
Apply suggestions from code review
d3dfeb5 
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
@fpvandoorn
Copy link
Member

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Jan 25, 2023
bors bot pushed a commit that referenced this pull request Jan 25, 2023
@urkud
Feat: add lemmas about Sum (#1583)
36eb75d 
This is the Lean 4 version of leanprover-community/mathlib#18184
@bors
Copy link

bors bot commented Jan 25, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Jan 25, 2023
@urkud
Feat: add lemmas about Sum (#1583)
cbc8391 
This is the Lean 4 version of leanprover-community/mathlib#18184
@bors
Copy link

bors bot commented Jan 25, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Jan 25, 2023
@urkud
Feat: add lemmas about Sum (#1583)
895e78b 
This is the Lean 4 version of leanprover-community/mathlib#18184
@bors
Copy link

bors bot commented Jan 25, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title Feat: add lemmas about Sum [Merged by Bors] - Feat: add lemmas about Sum Jan 25, 2023
@bors bors bot closed this Jan 25, 2023
@bors bors bot deleted the YK-sum-lemmas branch January 25, 2023 13:20
@eric-wieser eric-wieser mentioned this pull request Feb 13, 2023
Closed
bors bot pushed a commit that referenced this pull request Feb 22, 2023
@joneugster @eric-wieser
chore: update SHA of already forward-ported files (#2181)
88c789e 
Update some SHAs of files that changed in mathlib3.

These 17 files need mainly only updated SHA as they've been only touched by backports or already have been forward-ported.

The relevant changes are:

* [Algebra.Group.Defs (#17884)](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/defs?range=41cf0cc2f528dd40a8f2db167ea4fb37b8fde7f3..2e0975f6a25dd3fbfb9e41556a77f075f6269748)
  * #945
* [Algebra.Group.WithOne.Defs (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/with_one/defs?range=e574b1a4e891376b0ef974b926da39e05da12a06..995b47e555f1b6297c7cf16855f1023e355219fb)
  * #1439
* [Algebra.Module.Submodule.Basic (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/algebra/module/submodule/basic?range=f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c..feb99064803fd3108e37c18b0f77d0a8344677a3)
* [Algebra.Order.Monoid.WithTop (#18149, #18081)](https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/monoid/with_top?range=2258b40dacd2942571c8ce136215350c702dc78f..e7e2ba8aa216a5833b5ed85a93317263711a36b5)
  * #1508
  * #1439
* [Algebra.Order.Ring.WithTop (#18149, #18081)](https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/ring/with_top?range=550b58538991c8977703fdeb7c9d51a5aa27df11..e7e2ba8aa216a5833b5ed85a93317263711a36b5)
  * #1508
  * #1439
* [Data.Finset.NAry (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/data/finset/n_ary?range=9003f28797c0664a49e4179487267c494477d853..995b47e555f1b6297c7cf16855f1023e355219fb)
  * #1439
* [Data.Option.NAry (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/data/option/n_ary?range=2258b40dacd2942571c8ce136215350c702dc78f..995b47e555f1b6297c7cf16855f1023e355219fb)
  * #1439
* [Data.Set.NAry (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/data/set/n_ary?range=2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c..995b47e555f1b6297c7cf16855f1023e355219fb)
  * #1439
* [Data.SetLike.Basic (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/data/set_like/basic?range=fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e..feb99064803fd3108e37c18b0f77d0a8344677a3)
* [Data.Sum.Basic (#18184)](https://leanprover-community.github.io/mathlib-port-status/file/data/sum/basic?range=d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d..f4ecb599422baaf39055d8278c7d9ef3b5b72b88)
  * #1583
* [GroupTheory.GroupAction.SubMulAction  (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/group_action/sub_mul_action?range=f93c11933efbc3c2f0299e47b8ff83e9b539cbf6..feb99064803fd3108e37c18b0f77d0a8344677a3)
* [GroupTheory.Submonoid.Basic (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/submonoid/basic?range=207cfac9fcd06138865b5d04f7091e46d9320432..feb99064803fd3108e37c18b0f77d0a8344677a3)
* [ Logic.Basic (#18291): backport](https://leanprover-community.github.io/mathlib-port-status/file/logic/basic?range=1c521b4fb909320eca16b2bb6f8b5b0490b1cb5e..feb99064803fd3108e37c18b0f77d0a8344677a3)
  * #1509
* [Order.InitialSeg (#18198): backport](https://leanprover-community.github.io/mathlib-port-status/file/order/initial_seg?range=ee0c179cd3c8a45aa5bffbf1b41d8dbede452865..7c3269ca3fa4c0c19e4d127cd7151edbdbf99ed4)
* [Order.RelClasses (#17957)](https://leanprover-community.github.io/mathlib-port-status/file/order/rel_classes?range=c4658a649d216f57e99621708b09dcb3dcccbd23..bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e)
  * #1047
* [Order.WithBot (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/order/with_bot?range=70d50ecfd4900dd6d328da39ab7ebd516abe4025..995b47e555f1b6297c7cf16855f1023e355219fb)
  * #1439
* [RingTheory.Subsemiring.Basic (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/ring_theory/subsemiring/basic?range=f93c11933efbc3c2f0299e47b8ff83e9b539cbf6..feb99064803fd3108e37c18b0f77d0a8344677a3)



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kbuzzard kbuzzard kbuzzard approved these changes

Assignees
No one assigned
Labels
mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@urkud @fpvandoorn @kbuzzard