-
Notifications
You must be signed in to change notification settings - Fork 299
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(data/nat/unique_factorization): a unique_factorization_monoid
instance on N
#4194
Conversation
Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
unique_factorization_monoid
instance on N (deps: #4156)unique_factorization_monoid
instance on 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.
Some minor suggestions, it looks good otherwise!
section unique_units | ||
variables [monoid α] [unique (units α)] | ||
|
||
theorem associated_iff_eq {x y : α} : x ~ᵤ y ↔ x = y := |
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.
Remark that you shouldn't feel the need to follow up on: we also have the implication associated = eq → unique (units α)
from associated_one_iff_is_unit
.
import data.nat.prime | ||
import ring_theory.unique_factorization_domain | ||
|
||
theorem nat.prime_iff {p : ℕ} : p.prime ↔ prime p := |
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.
I never realized nat.prime
had its own incompatible definition! Can you move this theorem to data/nat/prime.lean
or will that cause cyclical imports?
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.
I made a new file, so as not to import algebra.associated
into data.nat.prime
for one lemma.
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.
Hmm, I'm a fan of small files but in this case I'm not sure. That nat.prime
is the same as _root_.prime
is a very fundamental result, so I would not expect it to be "hidden" in another file, as it were. And adding algebra.associated
to the imports of data.nat.prime
will only add two files to the import graph: algebra.associated
itself and data.multiset.basic
.
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.
Unfortunately, the proof of perm_of_prod_eq_prod
seems to be screwed up by importing data.multiset.basic
through algebra.associated
.
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.
Ah, I figured it out.
{ right, rw [hn, nat.is_unit_iff.1 un, mul_one], } } | ||
end | ||
|
||
namespace nat |
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.
I guess the above two lemmas aren't in the nat
namespace because it would interpret prime p
as nat.prime
, right? It looks a bit funny though.
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.
Exactly. I should look into seeing how bad it'd be to replace nat.prime
altogether.
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.
It sounds like a good way to get rid of some spare time :)
✌️ awainverse can now approve this pull request. To approve and merge a pull request, simply reply with |
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.
Thank you 🎉
I'm happy with the changes as they are, except that I'm in favour of incorporating data.nat.associated
into data.nat.prime
. It won't cause me to reject the PR though, so I'll let you decide what happens to it.
bors d+
unique_factorization_monoid
instance on Nunique_factorization_monoid
instance on N
bors r+ |
Canceled. |
bors r+ |
…instance on N (#4194) Provides a `unique_factorization_monoid` instance on `nat` Shows its equivalence to `nat.factors`, which is list-valued Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
unique_factorization_monoid
instance on Nunique_factorization_monoid
instance on N
Provides a
unique_factorization_monoid
instance onnat
Shows its equivalence to
nat.factors
, which is list-valued