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.Algebra.Prod #2383

Closed
wants to merge 26 commits into from
Closed

[Merged by Bors] - feat: port Algebra.Algebra.Prod #2383

wants to merge 26 commits into from

Conversation

Komyyy
Copy link
Collaborator

@Komyyy Komyyy commented Feb 20, 2023 •
edited by github-actions bot

@Komyyy
feat: port Algebra.Algebra.Hom
0eca982
@Komyyy
Initial file copy from mathport
3d53384
@Komyyy
automated fixes
3998abb 
Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
@Komyyy
62 red errors left
8674760
@Komyyy
40 red errors left
b9a11ca
@Komyyy
5 red errors left
2937c98
@Komyyy
add map_bit1
ffb8b1e
@Komyyy
1 red error left
5d7ab89
@Komyyy
no orange errors anymore
32b26e5
@Komyyy
mini lints
21af8e0
@Komyyy
no red errors anymore
8d4fb77
@Komyyy
naming conventions & docs
b479851
@Komyyy
no build lints anymore
ba3444e
@Komyyy
Merge branch 'master' into port/Algebra.Algebra.Hom
df5542a
@Komyyy
feat: port Algebra.Algebra.Prod
6a2148a
@Komyyy
Initial file copy from mathport
2daf068
@Komyyy
automated fixes
ce46572 
Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
@Komyyy
Merge branch 'port/Algebra.Algebra.Hom' into port/Algebra.Algebra.Prod
1ecfb5d
@Komyyy
name instances in Algebra.Module.Prod
5d78632
@Komyyy
generalize RingHom.coe_mk & RingHom.coe_monoidHom_mk
5bf07a0
@Komyyy
generalize AlgHom.coe_mk
5c8d2ba
@Komyyy
fix
329a262
@Komyyy Komyyy added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. blocked-by-other-PR This PR depends on another PR which is still in the queue. labels Feb 20, 2023
@Komyyy Komyyy removed the WIP Work in progress label Feb 20, 2023
@Komyyy Komyyy added awaiting-review The author would like community review of the PR and removed awaiting-review The author would like community review of the PR labels Feb 21, 2023
@semorrison semorrison removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Feb 21, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

@semorrison semorrison added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Feb 21, 2023
@jcommelin
Copy link
Member

Thanks 🎉

bors merge

@bors
Copy link

bors bot commented Feb 21, 2023

👎 Rejected by label

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Feb 21, 2023
@jcommelin jcommelin removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Feb 21, 2023
@jcommelin
Copy link
Member

bors r+

bors bot pushed a commit that referenced this pull request Feb 21, 2023
@Komyyy @jcommelin
feat: port Algebra.Algebra.Prod (#2383)
d9fac07 
Co-authored-by: Johan Commelin <johan@commelin.net>
@bors
Copy link

bors bot commented Feb 21, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Algebra.Algebra.Prod [Merged by Bors] - feat: port Algebra.Algebra.Prod Feb 21, 2023
@bors bors bot closed this Feb 21, 2023
@bors bors bot deleted the port/Algebra.Algebra.Prod branch February 21, 2023 10:19
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
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.

None yet
3 participants
@Komyyy @semorrison @jcommelin