-
Notifications
You must be signed in to change notification settings - Fork 251
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.
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
[Merged by Bors] - feat: Port RingTheory/RingInvo #1276
Conversation
Mathlib/RingTheory/RingInvo.lean
Outdated
@[simp] | ||
theorem map_eq_zero_iff (f : RingInvo R) {x : R} : f x = 0 ↔ x = 0 := | ||
f.toRingEquiv.map_eq_zero_iff | ||
#align ring_invo.map_eq_zero_iff RingInvo.map_eq_zero_iff |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@[simp] | |
theorem map_eq_zero_iff (f : RingInvo R) {x : R} : f x = 0 ↔ x = 0 := | |
f.toRingEquiv.map_eq_zero_iff | |
#align ring_invo.map_eq_zero_iff RingInvo.map_eq_zero_iff | |
/- Porting note `simp` attribute removed as suggested by linter: | |
simp can prove this: | |
by simp only [AddEquivClass.map_eq_zero_iff] | |
#noalign ring_invo.map_eq_zero_iff |
Again I'm not sure how to handle the linter error here correcty. If one replaces f x
by f.toRingEquiv
as above, the linter says it is no needed anymore.
The whole RingInvoClass business needs to be backported before we can merge this PR. The mathlib3 PR for this is found here. I'm removing the WIP, help, and question tags because I think this PR is finished up to these changes. |
The mathlib3 PR is merged now! I will wait to see how mathport translates that file once that happens, and then we can finish things up here :) |
All that's left is to decide whether we want |
Co-authored-by: Johan Commelin <johan@commelin.net>
…unity/mathlib4 into port/RingTheory.RingInvo
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
Everything compiles properly, not done with style/removing unnecisary lemmas Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: qawbecrdtey <qawbecrdtey@kaist.ac.kr> Co-authored-by: Lukas Miaskiwskyi <lukas.mias@gmail.com> Co-authored-by: z <32079362+zaxioms@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded:
|
Everything compiles properly, not done with style/removing unnecisary lemmas