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/group_action_hom, data/equiv/mul_add}): add missing inverse defs #7847

Closed
wants to merge 7 commits into from
Closed

[Merged by Bors] - feat({algebra/group_action_hom, data/equiv/mul_add}): add missing inverse defs #7847

wants to merge 7 commits into from

Conversation

ocfnash
Copy link
Collaborator

@ocfnash ocfnash commented Jun 8, 2021 •
edited

Open in Gitpod

@ocfnash
feat(algebra/non_unital_alg_hom): define non_unital_alg_hom
4dea920 
The motivation is to be able to state the universal property
for a magma algebra using bundled morphisms.
@ocfnash ocfnash added the awaiting-review The author would like community review of the PR label Jun 8, 2021
@ocfnash ocfnash mentioned this pull request Jun 9, 2021
Closed
1 task
@ocfnash
Drop addition of non_unital_alg_hom.lean
880e44b 
The plan is to split this PR in two since the other changes are
deep and cause long build times.
@ocfnash ocfnash changed the title feat(algebra/non_unital_alg_hom): define non_unital_alg_hom feat({algebra/group_action_hom, data/equiv/mul_add}): add missing inverse defs Jun 9, 2021
@ocfnash ocfnash mentioned this pull request Jun 9, 2021
Closed
1 task
Vierkantor
Vierkantor approved these changes Jun 11, 2021
View reviewed changes
Copy link
Collaborator

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

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

Thanks!

bors r+

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jun 11, 2021
kbuzzard
kbuzzard approved these changes Jun 11, 2021
View reviewed changes
src/algebra/group_action_hom.lean
@@ -124,10 +135,12 @@ instance has_coe' : has_coe (A →+[M] B) (A →[M] B) :=
⟨to_mul_action_hom⟩

instance : has_coe_to_fun (A →+[M] B) :=
⟨_, λ c, c.to_fun⟩
⟨_, to_fun⟩
Copy link
Member

Choose a reason for hiding this comment

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

There's another one of these on line 238

bors bot pushed a commit that referenced this pull request Jun 11, 2021
@ocfnash
feat({algebra/group_action_hom, data/equiv/mul_add}): add missing `in…
ff44ed5 
…verse` defs (#7847)
@bors
Copy link

bors bot commented Jun 12, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat({algebra/group_action_hom, data/equiv/mul_add}): add missing inverse defs [Merged by Bors] - feat({algebra/group_action_hom, data/equiv/mul_add}): add missing inverse defs Jun 12, 2021
@bors bors bot closed this Jun 12, 2021
@bors bors bot deleted the non_unital_alg_hom branch June 12, 2021 02:37
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 left review comments

@Vierkantor Vierkantor Vierkantor approved these changes

@kbuzzard kbuzzard kbuzzard approved these changes

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@ocfnash @eric-wieser @Vierkantor @kbuzzard