[Merged by Bors] - feat(algebra/module/basic): weaken assumption #16673
Conversation
negiizhao
commented
Sep 27, 2022
negiizhao
commented
negiizhao
added
awaiting-review
github-actions
bot
removed
the
awaiting-CI
src/algebra/module/basic.lean
Outdated
| @@ -617,7 +617,7 @@ end module | |||
|
|
|||
| section division_ring | |||
|
|
|||
| variables [division_ring R] [add_comm_group M] [module R M] | |||
| variables [division_ring R] [add_comm_monoid M] [module R M] | |||
There was a problem hiding this comment.
@YaelDillies, do we have division semirings now?
There was a problem hiding this comment.
Oh yes, and it can even be [group_with_zero R] [add_monoid M] [distrib_mul_action R M]. Should we use this?
There was a problem hiding this comment.
The distinction between group_with_zero and division_semiring is irrelevant here currently I suspect, but we definitely want at least division_semiring to be able to apply it to nnreal and nnrat.
There was a problem hiding this comment.
I suggest to go with division_semiring, that is mathematically more meaningful.
There was a problem hiding this comment.
Oh, I see you already have the more general version. No worries!
bors d+
There was a problem hiding this comment.
Doesn't hurt to have the extra generality, but indeed I can't come up with an example where it would be useful.
There was a problem hiding this comment.
You can maybe add a comment explaining that this applies to division_semiring, in particular nnreal.
|
✌️ negiizhao can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
|
|
||
| variables [division_ring R] [add_comm_group M] [module R M] | ||
| variables [group_with_zero R] [add_monoid M] [distrib_mul_action R M] |
There was a problem hiding this comment.
Presumably this no longer needs to be in this file now that it's not about module
bors r-
|
Canceled. |
|
✌️ negiizhao can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Split from #16412. All of the following lemmas move from namespace `is_scalar_tower` to namespace `polynomial`. Rename `aeval_apply` to `aeval_map_algebra_map` and swap the sides of the equality, remove `aeval_map` which is just the same as `aeval_map_algebra_map`. Rename `algebra_map_aeval` to `aeval_algebra_map_apply` and swap the sides of the equality, rename original `aeval_algebra_map_apply` to `aeval_algebra_map_apply_eq_algebra_map_eval`. Make the new lemma a `simp` lemma and remove `simp` from the original one. Rename `aeval_eq_zero_of_aeval_algebra_map_eq_zero` to `aeval_algebra_map_eq_zero_iff_of_injective` and make it an iff lemma. Replace `aeval_eq_zero_of_aeval_algebra_map_eq_zero_field` by `aeval_algebra_map_eq_zero_iff`, it has weaker assumptions and is also an iff lemma. - [x] depends on: #16673
