-
Notifications
You must be signed in to change notification settings - Fork 298
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(ring_theory/ideal/operations): add span_singleton_mul_left lemmas #18056
Conversation
Multramate
commented
Jan 3, 2023
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 🎉
maintainer merge
@@ -443,6 +443,31 @@ lemma span_singleton_mul_le_span_singleton_mul {x y : R} {I J : ideal R} : | |||
span {x} * I ≤ span {y} * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ := | |||
by simp only [span_singleton_mul_le_iff, mem_span_singleton_mul, eq_comm] | |||
|
|||
lemma span_singleton_mul_right_mono [is_domain R] {x : R} (hx : x ≠ 0) : | |||
span {x} * I ≤ span {x} * J ↔ I ≤ J := |
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.
One advantage of using submodule.pointwise_distrib_mul_action is that it doesn't require the semiring to be commutative, while ideal.has_mul requires it and hence doesn't allow you to state the noncommutative version. But let's not worry about that now.
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
1 similar comment
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
Thanks! bors mege |
bors merge |
Build failed (retrying...): |
Pull request successfully merged into master. Build succeeded: |