Skip to content

[Merged by Bors] - feat: port Algebra.Associated#1098

Closed
siddhartha-gadgil wants to merge 73 commits intomasterfrom
algebra_associated
Closed

[Merged by Bors] - feat: port Algebra.Associated#1098
siddhartha-gadgil wants to merge 73 commits intomasterfrom
algebra_associated

Conversation

@siddhartha-gadgil
Copy link
Copy Markdown
Collaborator

@siddhartha-gadgil siddhartha-gadgil commented Dec 19, 2022 •
edited by Ruben-VandeVelde
Loading

siddhartha-gadgil and others added 30 commits December 15, 2022 15:52
@siddhartha-gadgil
all but one error fixed
5e305ca
@siddhartha-gadgil
clean up, de-duplicate
39fa0c6
@siddhartha-gadgil
breaking lines
6b2f26e
@riccardobrasca
feat port Data.Nat.Pow
a6660ed
@riccardobrasca
update mathlib.lean
2e911fa
@riccardobrasca
green
67077a5
@riccardobrasca
port
b09ca1b
@riccardobrasca
start remove cyclic import
82a6e93
@riccardobrasca
Merge remote-tracking branch 'origin/master' into RB/group_power.lemmas
2c626d5
@riccardobrasca
revert this
7e6e81a
@riccardobrasca
remove dependency on norm_num
741f740
@riccardobrasca
let's start
7b856ee
@riccardobrasca
little progress
e2c2b74
@riccardobrasca
Merge remote-tracking branch 'origin/master' into RB/group_power.lemmas
202d926
@riccardobrasca
add simp tag
a0505ba
@riccardobrasca
add bit0_neg
93aeae3
@riccardobrasca
progress
df7e85c
@riccardobrasca
add align
3cde095
@riccardobrasca
more progress
7f805a7
@riccardobrasca
remove exit
cb06658
@siddhartha-gadgil
a couple of small fixes
48ac619
@siddhartha-gadgil
a few fixes
cade289
@siddhartha-gadgil
another set of fixes
24dab78
@siddhartha-gadgil
another set of fixes
605b18c
@siddhartha-gadgil
Merge branch 'master' into RB/group_power.lemmas
415d611
@siddhartha-gadgil
fixed ../GroupPower/Lemmas; broke NormNum
8eebf91
@siddhartha-gadgil
porting notes added
6fcdc00
@siddhartha-gadgil
restored ad hoc theorem
48f8407
@siddhartha-gadgil
broke line
46316df
@siddhartha-gadgil
got rid of linting errors
9ca9a82
@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 19, 2022
@kim-em kim-em 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 19, 2022
Ruben-VandeVelde
Ruben-VandeVelde requested changes Dec 19, 2022
View reviewed changes
Copy link
Copy Markdown
Contributor

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

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

Needs another careful review of the names.

@kim-em kim-em added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Dec 19, 2022
siddhartha-gadgil and others added 5 commits December 20, 2022 06:08
@siddhartha-gadgil @Ruben-VandeVelde
Update Mathlib/Algebra/Associated.lean
5949ffd 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@siddhartha-gadgil @Ruben-VandeVelde
Update Mathlib/Algebra/Associated.lean
6baaba5 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@siddhartha-gadgil @Ruben-VandeVelde
Update Mathlib/Algebra/Associated.lean
f2a3894 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@siddhartha-gadgil @Ruben-VandeVelde
Update Mathlib/Algebra/Associated.lean
f73ec6a 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@siddhartha-gadgil
fixes based on review
99ad32a
@siddhartha-gadgil siddhartha-gadgil added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Dec 20, 2022
kim-em and others added 2 commits December 20, 2022 16:17
@kim-em @Ruben-VandeVelde
Update Mathlib/Algebra/Associated.lean
c568c52 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@kim-em @Ruben-VandeVelde
Apply suggestions from code review
ba64f38 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
kim-em
kim-em reviewed Dec 20, 2022
View reviewed changes
@kim-em @Ruben-VandeVelde
Apply suggestions from code review
b01f965 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Dec 20, 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 20, 2022
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>
@siddhartha-gadgil siddhartha-gadgil removed the request for review from Ruben-VandeVelde December 20, 2022 05:47
@bors
Copy link
Copy Markdown

bors bot commented Dec 20, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Algebra.Associated [Merged by Bors] - feat: port Algebra.Associated Dec 20, 2022
@bors bors bot closed this Dec 20, 2022
@bors bors bot deleted the algebra_associated branch December 20, 2022 05:52
@github-actions github-actions bot mentioned this pull request Dec 20, 2022
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

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde requested changes

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

@siddhartha-gadgil @kim-em @Ruben-VandeVelde @riccardobrasca @ChrisHughes24