Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

feat(algebra/parity): Squares and primality #12992

Open
khwilson wants to merge 84 commits into
base: master
Choose a base branch
from
Open

feat(algebra/parity): Squares and primality #12992

khwilson wants to merge 84 commits into from

Conversation

@khwilson
Copy link
Collaborator

@khwilson khwilson commented Mar 27, 2022 •
edited by github-actions bot
Loading

Introduce some decidability predicates for N and Z while also proving that a natural number is a square if and only if every one of its (maximal) prime power divisors is an even power.

Open in Gitpod

adomani and others added 8 commits March 22, 2022 13:20
@adomani
prepare to_additive to convert square -> even
6980b23
@adomani
move defs of even/odd to algebra.parity file
a0e87ef
@adomani
gather even/odd in a comprehensive file
76457da
@adomani
even first, odd later
e23ff2e
@adomani
Merge remote-tracking branch 'origin/master' into adomani_prepare_eve…
20ee139 
…n_refactor
@adomani
change def
0554c65
@khwilson
feat(algebra/square): Add the notion of "square" elements of monoids
47417f0 
There is already a concept of `even` and `odd`, but not of `square`.
These are some initial lemmas about being a square that I use in the
proof of the density of squarefree integers.

Note that this also introduces the notation `sqrt0`, which is `0` if its
argument is not a square and otherwise is its squareroot. This is in
line with `real.sqrt`'s behavior on negative numbers. However, the name
perhaps could use some work?
@khwilson
Linting
1caa272
@khwilson khwilson added the awaiting-review The author would like community review of the PR label Mar 27, 2022
vihdzp
vihdzp reviewed Mar 28, 2022
View reviewed changes
Copy link
Collaborator

@vihdzp vihdzp left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

tl;dr there's tons of golfing to be done, and also you should look into whether your theorems can be generalized if you don't already plan on doing so.

khwilson and others added 6 commits March 28, 2022 08:00
@khwilson @vihdzp
Update src/algebra/square.lean
9b7be26 
Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>
@khwilson @vihdzp
Update src/algebra/square.lean
c9d591e 
Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>
@khwilson @vihdzp
Update src/algebra/square.lean
1e7f641 
Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>
@khwilson
Extraneous end
7064ea4
@khwilson
Split out square_mul into sublemmas
a75521e
@khwilson
Further golfing
2681a74
@khwilson
Copy link
Collaborator Author

khwilson commented Mar 28, 2022

Thanks for the review @vihdzp ! Comments addressed, with a couple questions inline :-)

@khwilson
Copy link
Collaborator Author

khwilson commented Mar 28, 2022

Thanks again @vihdzp . Responded to your comments and added a long note in the code to address the UFM generalization

@Ruben-VandeVelde
Copy link
Collaborator

Ruben-VandeVelde commented Mar 29, 2022

I think @adomani was looking into this as well

@adomani
Copy link
Collaborator

adomani commented Mar 29, 2022

Yes, I am indeed going to add is_square (and even as its to_additive partner). This may take a few days though, since, at the moment, I have only moved most relevant even lemmas to the same file, but have not yet changed the definition.

YaelDillies
YaelDillies reviewed Apr 21, 2022
View reviewed changes
khwilson and others added 2 commits April 21, 2022 12:35
@khwilson @YaelDillies
Update src/data/nat/factorization.lean
723f4ca 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@khwilson @YaelDillies
Update src/data/nat/factorization.lean
9a1d7b7 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 22, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 24, 2022
@khwilson
Copy link
Collaborator Author

khwilson commented Apr 25, 2022

OK, assuming that this run goes fine, I think it's good to merge modulo one outstanding question from @jcommelin . So just bumping for him. :-)

@khwilson
Copy link
Collaborator Author

khwilson commented May 8, 2022

@jcommelin just bumping vis-a-vis the names! Thanks!!

@YaelDillies
Copy link
Collaborator

YaelDillies commented Sep 8, 2022

I just fixed the conflicts. I think that's ready?

@YaelDillies YaelDillies mentioned this pull request Sep 8, 2022
Closed
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Sep 8, 2022
@khwilson
Copy link
Collaborator Author

khwilson commented Sep 8, 2022

Thanks for coming back to this! It looks fine to me at this point, beyond the obvious build issues :-)

@YaelDillies
Copy link
Collaborator

YaelDillies commented Sep 8, 2022

I split off the changes in algebra.parity to #16430 (feel free to add a Co-authored-by line there with your email address!). I expect the rest of this PR to be verbatim generalisable to UFDs, so I'll try doing that once #16430 goes through.

@khwilson
Copy link
Collaborator Author

khwilson commented Sep 8, 2022

Oh, very nice. Not sure how to add a Co-authored-by, but appreciate it.

@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Sep 10, 2022
@mathlib-dependent-issues-bot
Copy link
Collaborator

mathlib-dependent-issues-bot commented Sep 10, 2022

This PR/issue depends on:

@jcommelin
Copy link
Member

jcommelin commented Sep 12, 2022

Build is failing...

@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 12, 2022
@kim-em kim-em added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

4 more reviewers

@jcommelin jcommelin jcommelin left review comments

@YaelDillies YaelDillies YaelDillies left review comments

@adomani adomani adomani left review comments

@vihdzp vihdzp vihdzp left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

awaiting-author A reviewer has asked the author a question or requested changes too-late This PR was ready too late for inclusion in mathlib3

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

10 participants

@khwilson @Ruben-VandeVelde @adomani @YaelDillies @mathlib-dependent-issues-bot @jcommelin @vihdzp @kim-em @leanprover-community-bot-assistant