[Merged by Bors] - feat(data/nat/gcd): add coprime_prod_left and coprime_prod_right #12268
Conversation
nomeata
commented
Feb 24, 2022
nomeata
commented
nomeata
added
the
awaiting-review
Any other reviewers with an opionion? |
|
|
||
| open_locale big_operators | ||
|
|
||
| lemma coprime_prod_left |
There was a problem hiding this comment.
Should we not prove these for unique_factorization_monoids rather than just ℕ?
There was a problem hiding this comment.
They are specializions from these: https://leanprover-community.github.io/mathlib_docs/ring_theory/coprime/lemmas.html#is_coprime.prod_left because it's hard to use them at N. Having a single notion of coprime and a single set of lemmas that works everywhere would be great.
There was a problem hiding this comment.
Oh I see, how unfortunate that nat.coprime has its own weird definition :-/
There was a problem hiding this comment.
(Even worse, nat.coprime is actually in the Lean library itself.)
|
Thanks for these. I think worth adding a reference to the more general versions https://leanprover-community.github.io/mathlib_docs/ring_theory/coprime/lemmas.html#is_coprime.prod_left (and right) in the doc strings but otherwise great. bors d+ |
|
✌️ nomeata can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
Bors merge |
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
