Skip to content

[Merged by Bors] - feat port Algebra.GroupPower.Lemmas#1055

Closed
riccardobrasca wants to merge 42 commits intomasterfrom
RB/group_power.lemmas
Closed

[Merged by Bors] - feat port Algebra.GroupPower.Lemmas#1055
riccardobrasca wants to merge 42 commits intomasterfrom
RB/group_power.lemmas

Conversation

@riccardobrasca
Copy link
Copy Markdown
Member

@riccardobrasca riccardobrasca commented Dec 15, 2022 •
edited by github-actions bot
Loading

@riccardobrasca riccardobrasca mentioned this pull request Dec 15, 2022
Closed
4 tasks
@riccardobrasca riccardobrasca added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Dec 15, 2022
@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 15, 2022
@riccardobrasca riccardobrasca removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 16, 2022
@kim-em kim-em added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Dec 18, 2022
@siddhartha-gadgil siddhartha-gadgil mentioned this pull request Dec 19, 2022
Closed
2 tasks
siddhartha-gadgil and others added 6 commits December 19, 2022 06:20
@siddhartha-gadgil @kbuzzard
Update Mathlib/Algebra/GroupPower/Lemmas.lean
afeaf27 
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
@siddhartha-gadgil @kbuzzard
Update Mathlib/Algebra/GroupPower/Lemmas.lean
f83b83b 
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
@siddhartha-gadgil
changes based on review
df46f66
@siddhartha-gadgil @kbuzzard
Update Mathlib/Algebra/GroupPower/Lemmas.lean
2206720 
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
@siddhartha-gadgil
more comments addressed
39af7b1
@siddhartha-gadgil
more fixes as per review
eb86f42
@siddhartha-gadgil siddhartha-gadgil added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Dec 19, 2022
@ChrisHughes24
Copy link
Copy Markdown
Member

ChrisHughes24 commented Dec 19, 2022

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Dec 19, 2022
bors bot pushed a commit that referenced this pull request Dec 19, 2022
@riccardobrasca @siddhartha-gadgil
feat port Algebra.GroupPower.Lemmas (#1055)
1bec125 
aba57d4d3dae35460225919dcd82fe91355162f9

- [x] depends on #1043 
- [x] depends on #1050  

Co-authored-by: Siddhartha Gadgil <siddhartha.gadgil@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Dec 19, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat port Algebra.GroupPower.Lemmas [Merged by Bors] - feat port Algebra.GroupPower.Lemmas Dec 19, 2022
@bors bors bot closed this Dec 19, 2022
@bors bors bot deleted the RB/group_power.lemmas branch December 19, 2022 11:40
@dwrensha dwrensha mentioned this pull request Dec 19, 2022
Closed
bors bot pushed a commit that referenced this pull request Dec 19, 2022
@siddhartha-gadgil @riccardobrasca
feat: port Algebra.Parity (#1092)
80b4179 
dcf2250875895376a142faeeac5eabff32c48655

- [x] depends on: #1055 

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
bors bot pushed a commit that referenced this pull request Dec 20, 2022
@siddhartha-gadgil @riccardobrasca
feat: port Algebra.Associated (#1098)
69dfd0b 
dcf2250875895376a142faeeac5eabff32c48655

* [x] depends on #1055
* [x] depends on #1092

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
bors bot pushed a commit that referenced this pull request Dec 20, 2022
@dwrensha
chore: remove remaining sorries in Abel.lean (#1106)
77f3e39 
Removes the remaining sorries in Abel.lean. This has been made possible by the landing of #1055. This is a continuation of #915.
bors bot pushed a commit that referenced this pull request Dec 21, 2022
@riccardobrasca @mcdoll
@winstonyin @ChrisHughes24
feat port Data.Int.Gcd (#981)
6a95868 
fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

- [x] depends on #1040  
- [x] depends on #1043
- [x] depends on #1050 
- [x] depends on #1055 

Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>
Co-authored-by: Winston Yin <winstonyin@gmail.com>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
bors bot pushed a commit that referenced this pull request Dec 21, 2022
@riccardobrasca @mcdoll
@winstonyin @ChrisHughes24
feat port Data.Int.Gcd (#981)
f666388 
fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

- [x] depends on #1040  
- [x] depends on #1043
- [x] depends on #1050 
- [x] depends on #1055 

Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>
Co-authored-by: Winston Yin <winstonyin@gmail.com>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
bors bot pushed a commit that referenced this pull request Dec 21, 2022
@riccardobrasca @mcdoll
@winstonyin @ChrisHughes24
feat port Data.Int.Gcd (#981)
8aa6d64 
fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

- [x] depends on #1040  
- [x] depends on #1043
- [x] depends on #1050 
- [x] depends on #1055 

Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>
Co-authored-by: Winston Yin <winstonyin@gmail.com>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
@dwrensha dwrensha mentioned this pull request Jan 3, 2023
Closed
bors bot pushed a commit that referenced this pull request Jan 3, 2023
@dwrensha
chore: remove duplicated definition of Invertible class in NormNum.Co…
3b9e5d4 
…re.lean (#1313)

* Deletes the temporary `Invertible` class defined in `NormNum.Core`. This is possible because `Algebra.Invertible` landed in #930, and its dependence on `NormNum` was removed in #1055.
* Updates the definition of the `Invertible.toInv` syntax to not require a space and to more closely match the `Inv.inv` syntax.
@Ruben-VandeVelde Ruben-VandeVelde mentioned this pull request Mar 23, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em left review comments

@kbuzzard kbuzzard kbuzzard approved these changes

+1 more reviewer

@siddhartha-gadgil siddhartha-gadgil siddhartha-gadgil left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

mathlib-port This is a port of a theory file from mathlib. 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.

5 participants

@riccardobrasca @ChrisHughes24 @kim-em @siddhartha-gadgil @kbuzzard