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
feat(number_theory/divisors): add divisors_mul #17041
base: master
Are you sure you want to change the base?
Conversation
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
I already have an open PR to change |
Do you have the |
No, since it's just a direct consequence of |
This PR/issue depends on: |
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's a golf
rcases m.eq_zero_or_pos with rfl | hm, | ||
{ simp }, | ||
rcases n.eq_zero_or_pos with rfl | hn, | ||
{ simp }, | ||
ext i, | ||
simp only [hm.ne', hn.ne', finset.mem_mul, mem_divisors, ne.def, nat.mul_eq_zero, or_self, | ||
not_false_iff, and_true, dvd_mul], |
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.
rcases m.eq_zero_or_pos with rfl | hm, | |
{ simp }, | |
rcases n.eq_zero_or_pos with rfl | hn, | |
{ simp }, | |
ext i, | |
simp only [hm.ne', hn.ne', finset.mem_mul, mem_divisors, ne.def, nat.mul_eq_zero, or_self, | |
not_false_iff, and_true, dvd_mul], | |
simp_rw [ext_iff, mem_mul, mem_divisors, dvd_mul, ←exists_and_distrib_right, mul_ne_zero_iff], | |
exact λ x, exists_congr (λ m, exists_congr (λ n, by tauto)), |
Extracted from this Zulip message.
Also fixes some bad indentation in nearby lemmas
Co-authored-by: Bhavik Mehta bhavikmehta8@gmail.com
nat.dvd_mul
anddvd_mul
#17131