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: Injectivity of monoid localization #9531
Conversation
Spaces and so on
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Removed a result and modifying according to review
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
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.
Here and elsewhere you should add spaces
Note that I do not really know how to use the review interface properly and some of the diffs above are not correct. |
Add spaces
I hope I added all the appropriate spaces.... |
A letter change
Co-authored-by: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Changed simp to simp_rw
Shorten the calc proof
Spaces Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Modify some text
Change by_contra with intro
Changed cases' with obtain
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
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.
Just a final stylistic comment: can you avoid having three intermediate results all called this
? Lean seems to be good in understanding which one to use (or maybe it uses the last one, I am not sure), but this looks like a code smell.
Thanks!
bors d+
✌️ XavierXarles can now approve this pull request. To approve and merge a pull request, simply reply with |
I have the impression you really like to make a lot of intermediate statement using -- The hypothesis `h` gives that `f` (so, `g`) is injective, and we can cancel out `b.1`.
have : b.1 * (y.1 * x.2) = b.1 * (x.1 * y.2) :=
(LocalizationMap.toMap_injective_iff fl).mpr h this
rw [mul_comm, ← IsLeftCancelMulZero.mul_left_cancel_of_ne_zero b1ne0 this, mul_comm] |
Another stylistic comment: I think |
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Changed the proof acording to suggerences
lint Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
bors r+ |
Adds two results on the Localization for CommMonoids: one, describes exactly when the localization map is injective, the other essentially says that the localization of a cancellative Monoid is cancellative if the localization is injective. Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
[IsCancelMulZero M] (h : ∀ ⦃x⦄, x ∈ S → IsRegular x): IsCancelMulZero N := by | ||
have:IsLeftCancelMulZero N:= |
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.
lacking some spaces here; maybe fix in your next PR
[IsCancelMulZero M] (h : ∀ ⦃x⦄, x ∈ S → IsRegular x) : IsCancelMulZero N := by
have : IsLeftCancelMulZero N :=
Adds two results on the Localization for CommMonoids: one, describes exactly when the localization map is injective, the
other essentially says that the localization of a cancellative Monoid is cancellative if the localization is injective.