feat (data/pnat): extensions to pnat #1073
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
jcommelin
reviewed
May 21, 2019
Co-Authored-By: Johan Commelin <johan@commelin.net>
Co-Authored-By: Johan Commelin <johan@commelin.net>
ChrisHughes24
previously requested changes
May 23, 2019
src/data/pnat/basic.lean
Outdated
| we used the general monoid version. | ||
| -/ | ||
| instance : has_pow ℕ+ ℕ := ⟨λ n m, ⟨n.1 ^ m, nat.pow_pos n.2 m⟩⟩ | ||
|
|
There was a problem hiding this comment.
I don't think this is necessary. The main reason there's a separate has_pow for nat is that it is in core. Having two separate definitions causes a few problems, so we should really use monoid.pow
There was a problem hiding this comment.
I have switched to using monoid.pow, and put in a proof that coercion preserves powers.
mergify
bot
dismissed
ChrisHughes24’s stale review
Pull request has been modified.
6 tasks
ChrisHughes24
previously requested changes
Jun 5, 2019
src/data/pnat/xgcd.lean
Outdated
| theorem is_reduced_iff : u.is_reduced ↔ u.is_reduced' := | ||
| ⟨congr_arg succ_pnat, succ_pnat_inj⟩ | ||
|
|
||
| def flip' : ℕ × ℕ → ℕ × ℕ := λ v, ⟨v.2, v.1⟩ |
There was a problem hiding this comment.
I have switched to using prod.swap
src/data/pnat/xgcd.lean
Outdated
|
|
||
| theorem gcd_rel_right' : | ||
| (gcd_w a b) * (gcd_b' a b) = succ_pnat ((gcd_y a b) * (gcd_a' a b)) := | ||
| (gcd_props a b).2.2.2.2.1 |
There was a problem hiding this comment.
proofs shouldn't be indented.
There was a problem hiding this comment.
I have fixed this, and various other formatting issues.
mergify
bot
dismissed
ChrisHughes24’s stale review
Pull request has been modified.
ChrisHughes24
approved these changes
Jun 10, 2019
anrddh
pushed a commit
to anrddh/mathlib
that referenced
this pull request
May 15, 2020
* Extended API, especially divisibility and primes * Positive euclidean algorithm * Disambiguate overloaded :: * Tweak broken proof of flip_is_special * Change to mathlib style * Update src/data/pnat.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/data/pnat.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Adjust style for mathlib * Moved and renamed * Move some material from basic.lean to prime.lean * Move some material from basic.lean to factors.lean * Update import to data.pnat.basic. * Update import to data.pnat.basic * Fix import of data.pnat.basic * Use monoid.pow instead of nat.pow * Fix pnat.pow_succ -> pow_succ; stylistic changes * More systematic use of coercion * More consistent use of coercion * Formatting; change flip' to prod.swap
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This adds lots of thing to the type pnat of positive integers. Many of them are related
to divisibility and prime factorization, which work most nicely in the pnat context.
Specifically, we construct an equivalence between pnat and the type of multisets
of primes, and prove that this respects various structures. This is closely related
to the content of ring_theory/unique_factorization_domain.lean, but not quite
the same because there are no units and so factorization is actually unique.
There is also (in pnat_xgcd.lean) a version of the extended Euclidean algorithm that
works purely in nat and pnat rather than int. This is useful because it interacts well
with the theory of continued fractions and the structure theory of SL_2(N).
Moreover, there is a clear uniqueness property for the output of this algorithm,
which is not so obvious for the integer version.
UPDATE: after the original version of this PR
This is my first attempt to add any meaningful content to mathlib. Please let me know if there are general things that I should be doing differently.
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list