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: port Algebra.MonoidAlgebra.Division #3068

Closed
wants to merge 19 commits into from
Closed

[Merged by Bors] - feat: port Algebra.MonoidAlgebra.Division #3068

wants to merge 19 commits into from

Conversation

Parcly-Taxel
Copy link
Collaborator

@Parcly-Taxel Parcly-Taxel commented Mar 24, 2023 •
edited by github-actions bot

@Parcly-Taxel Parcly-Taxel added help-wanted The author needs attention to resolve issues WIP Work in progress blocked-by-other-PR This PR depends on another PR which is still in the queue. mathlib-port This is a port of a theory file from mathlib. mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged labels Mar 24, 2023
@semorrison semorrison removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Mar 24, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

eric-wieser
eric-wieser approved these changes Mar 25, 2023
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

bors d+

Thanks!

@bors
Copy link

bors bot commented Mar 25, 2023

✌️ Parcly-Taxel 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 eric-wieser added awaiting-CI and removed help-wanted The author needs attention to resolve issues WIP Work in progress delegated mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged labels Mar 25, 2023
@Parcly-Taxel
Copy link
Collaborator Author

bors merge

bors bot pushed a commit that referenced this pull request Mar 25, 2023
@Parcly-Taxel @eric-wieser
feat: port Algebra.MonoidAlgebra.Division (#3068)
525ff05 
This is the second part of the forward port of leanprover-community/mathlib#15905.



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

bors bot commented Mar 25, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Algebra.MonoidAlgebra.Division [Merged by Bors] - feat: port Algebra.MonoidAlgebra.Division Mar 25, 2023
@bors bors bot closed this Mar 25, 2023
@bors bors bot deleted the port/Algebra.MonoidAlgebra.Division branch March 25, 2023 12:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser approved these changes

Assignees
No one assigned
Labels
awaiting-CI mathlib-port This is a port of a theory file from mathlib.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@Parcly-Taxel @semorrison @eric-wieser