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/*): star_ring instances on free_algebra, free_monoid, ring_quot, and quaternion #4902

Closed
wants to merge 28 commits into from
Closed

[Merged by Bors] - feat(algebra/*): star_ring instances on free_algebra, free_monoid, ring_quot, and quaternion #4902

wants to merge 28 commits into from

Conversation

eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Nov 4, 2020 •
edited by github-actions bot

@eric-wieser eric-wieser added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Nov 4, 2020
@eric-wieser eric-wieser mentioned this pull request Nov 4, 2020
Closed
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Nov 12, 2020
@eric-wieser
Merge remote-tracking branch 'origin/master' into free_algebra-star
074ab62 
# Conflicts:
#	src/algebra/star/algebra.lean
#	src/algebra/star/basic.lean
#	src/data/matrix/basic.lean
#	src/linear_algebra/tensor_algebra.lean
@eric-wieser
Remove dead code
d1d8907
@eric-wieser
Add simp lemmas
6874756
@eric-wieser eric-wieser removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Nov 16, 2020
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Nov 16, 2020
@eric-wieser eric-wieser added the WIP Work in progress label Nov 16, 2020
@eric-wieser eric-wieser changed the title feat(algebra/*): star_ring instances on free_algebra and friends feat(algebra/*): star_ring instances on free_algebra and quaternion Nov 17, 2020
@eric-wieser eric-wieser added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Nov 17, 2020
@eric-wieser eric-wieser changed the title feat(algebra/*): star_ring instances on free_algebra and quaternion feat(algebra/*): star_ring instances on free_algebra, free_monoid, ring_quot, and quaternion Nov 17, 2020
@eric-wieser
Copy link
Member Author

eric-wieser commented Nov 17, 2020 •
edited

Decided to leave out tensor_algebra, exterior_algebra, etc for now, since to do those I either need to:

jcommelin
jcommelin reviewed Nov 18, 2020
View reviewed changes
src/algebra/free_algebra.lean Outdated Show resolved Hide resolved
src/algebra/free_monoid.lean Show resolved Hide resolved
jcommelin
jcommelin approved these changes Nov 19, 2020
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

LGTM. If you address the open remarks, then this can be merged.

bors d+

src/algebra/free_algebra.lean Outdated Show resolved Hide resolved
src/algebra/free_monoid.lean Show resolved Hide resolved
@bors
Copy link

bors bot commented Nov 19, 2020

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@eric-wieser @jcommelin
Apply suggestions from code review
664394e 
Co-authored-by: Johan Commelin <johan@commelin.net>
@eric-wieser
Copy link
Member Author

bors r+

bors bot pushed a commit that referenced this pull request Nov 19, 2020
@semorrison @eric-wieser
feat(algebra/*): star_ring instances on free_algebra, free_monoid, ri…
b479d3b 
…ng_quot, and quaternion (#4902)

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@bors
Copy link

bors bot commented Nov 19, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra/*): star_ring instances on free_algebra, free_monoid, ring_quot, and quaternion [Merged by Bors] - feat(algebra/*): star_ring instances on free_algebra, free_monoid, ring_quot, and quaternion Nov 19, 2020
@bors bors bot closed this Nov 19, 2020
@bors bors bot deleted the free_algebra-star branch November 19, 2020 15:34
@YaelDillies YaelDillies removed the awaiting-review The author would like community review of the PR label Nov 15, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@eric-wieser @jcommelin @YaelDillies @semorrison