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): star_linear_equiv #9426

Closed
wants to merge 26 commits into from
Closed

[Merged by Bors] - feat(algebra/star): star_linear_equiv #9426

wants to merge 26 commits into from

Conversation

eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Sep 28, 2021 •
edited by github-actions bot

@github-actions github-actions bot 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 Sep 28, 2021
@github-actions github-actions bot 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 Sep 28, 2021
@github-actions github-actions bot 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 Sep 29, 2021
@eric-wieser
Merge branch 'eric-wieser/star-opposite' into eric-wieser/star_linear…
5e4b27f 
…_map

# Conflicts:
#	src/algebra/star/basic.lean
@github-actions github-actions bot 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 Sep 30, 2021
@github-actions github-actions bot 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 Oct 1, 2021
@eric-wieser eric-wieser mentioned this pull request Oct 1, 2021
Closed
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 2, 2021
@github-actions github-actions bot added blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. merge-conflict Please `git merge origin/master` then a bot will remove this label. labels Oct 2, 2021
@dupuisf
Copy link
Collaborator

dupuisf commented Oct 2, 2021

I just added the ring_hom_inv_pair instance needed to define star-linear maps over commutative star-rings (i.e. conjugate-linear maps).

@dupuisf
Copy link
Collaborator

dupuisf commented Oct 5, 2021

I have now redefined star_linear_equiv to be specialized to commutative R, and renamed the initial noncommutative definition star_linear_equiv_nc. This is to avoid having to deal with op in the commutative case.

@dupuisf dupuisf self-assigned this Oct 5, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 10, 2021
@bryangingechen bryangingechen added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 10, 2021
@dupuisf dupuisf added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 10, 2021
dupuisf and others added 2 commits October 10, 2021 19:30
@dupuisf @hrmacbeth
Update src/algebra/star/module.lean
53ec52e 
Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
@dupuisf
commit suggestions
0bf8a03
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 13, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 13, 2021
@hrmacbeth
Copy link
Member

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 Oct 14, 2021
bors bot pushed a commit that referenced this pull request Oct 14, 2021
@eric-wieser @dupuisf
feat(algebra/star): star_linear_equiv (#9426)
c12aced 
Co-authored-by: Frédéric Dupuis <dupuisf@iro.umontreal.ca>
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
@bors
Copy link

bors bot commented Oct 14, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra/star): star_linear_equiv [Merged by Bors] - feat(algebra/star): star_linear_equiv Oct 14, 2021
@bors bors bot closed this Oct 14, 2021
@bors bors bot deleted the eric-wieser/star_linear_map branch October 14, 2021 23:10
@hrmacbeth hrmacbeth mentioned this pull request Oct 28, 2021
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

@dupuisf dupuisf dupuisf left review comments

@hrmacbeth hrmacbeth hrmacbeth approved these changes

Assignees

@dupuisf dupuisf

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
5 participants
@eric-wieser @dupuisf @hrmacbeth @urkud @bryangingechen