Skip to content

[Merged by Bors] - feat: port Algebra.Ring.Equiv#1077

Closed
ADedecker wants to merge 18 commits intomasterfrom
AD_PORT_RingEquiv
Closed

[Merged by Bors] - feat: port Algebra.Ring.Equiv#1077
ADedecker wants to merge 18 commits intomasterfrom
AD_PORT_RingEquiv

Conversation

@ADedecker
Copy link
Copy Markdown
Member

@ADedecker ADedecker commented Dec 16, 2022 •
edited
Loading

@ADedecker ADedecker added WIP Work in progress help-wanted The author needs attention to resolve issues labels Dec 16, 2022
@ADedecker ADedecker added awaiting-review and removed WIP Work in progress labels Dec 17, 2022
@ADedecker ADedecker added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 21, 2022
@kim-em kim-em removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 22, 2022
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Dec 22, 2022

This PR/issue depends on:

@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 22, 2022
@kim-em kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 23, 2022
@ADedecker ADedecker removed the help-wanted The author needs attention to resolve issues label Dec 23, 2022
jcommelin
jcommelin reviewed Dec 24, 2022
View reviewed changes
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Dec 24, 2022
@ADedecker ADedecker removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 24, 2022
@ChrisHughes24 ChrisHughes24 added the mathlib-port This is a port of a theory file from mathlib. label Dec 26, 2022
@ChrisHughes24
Copy link
Copy Markdown
Member

ChrisHughes24 commented Dec 26, 2022

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Dec 26, 2022
bors bot pushed a commit that referenced this pull request Dec 26, 2022
@ADedecker @ChrisHughes24
feat: port Algebra.Ring.Equiv (#1077)
84ee4ca 
See discussion [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/norm_cast.3A.20badly.20shaped.20lemma) and [there](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Algebra.2ERing.2EEquiv.20help.20request)

I used #835 as a reference

- [x] depends on: #1150

Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Dec 26, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Algebra.Ring.Equiv [Merged by Bors] - feat: port Algebra.Ring.Equiv Dec 26, 2022
@bors bors bot closed this Dec 26, 2022
@bors bors bot deleted the AD_PORT_RingEquiv branch December 26, 2022 15:11
@github-actions github-actions bot mentioned this pull request Dec 27, 2022
Closed
@eric-wieser eric-wieser mentioned this pull request Mar 21, 2023
Closed
bors bot pushed a commit that referenced this pull request Mar 21, 2023
@eric-wieser
fix: add incorrectly-deleted lemmas (#3008)
b0625e5 
These lemmas are still needed in Lean 4, despite claims in #1077 that they are not.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

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.

4 participants

@ADedecker @kim-em @ChrisHughes24 @jcommelin