mathlib3
feat(algebra/parity): Squares and primality
#12992
Open
Overview
Commits
84
Changes
View On GitHub

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

khwilson wants to merge 84 commits into master from add_square
khwilson
adomani prepare to_additive to convert square -> even
6980b232
adomani move defs of even/odd to algebra.parity file
a0e87ef5
adomani gather even/odd in a comprehensive file
76457da1
adomani even first, odd later
e23ff2e0
adomani Merge remote-tracking branch 'origin/master' into adomani_prepare_eve…
20ee1394
adomani change def
0554c654
khwilson feat(algebra/square): Add the notion of "square" elements of monoids
47417f06
khwilson Linting
1caa2724
khwilson khwilson added awaiting-review
khwilson More linting
feb9c6ce
vihdzp
vihdzp commented on 2022-03-28
khwilson Update src/algebra/square.lean
9b7be268
khwilson Update src/algebra/square.lean
c9d591ef
khwilson Update src/algebra/square.lean
1e7f6417
khwilson Extraneous end
7064ea42
khwilson Split out square_mul into sublemmas
a75521e6
khwilson Further golfing
2681a740
khwilson
khwilson Further PR requests
74cd9b6d
khwilson
Ruben-VandeVelde
adomani
adomani Merge remote-tracking branch 'origin/master' into adomani_squeven
b602c634
adomani partial
b245426a
adomani Merge branch 'master' into adomani_squeven
27cf14fa
adomani more partial
a97fbcdc
adomani fix
84da9ef8
adomani Merge remote-tracking branch 'origin/master' into adomani_squeven
4984af53
adomani more changes
05b0f0c4
adomani latest
543ae5be
adomani
adomani
khwilson
khwilson
adomani fix nat_parity
f1d2ce02
adomani fix int.parity
432e7fa6
adomani
adomani fix primorial
869f58c9
adomani add todo
74158440
adomani fix periodic
c0f1295b
adomani fix degree_sum
aa39b293
adomani fix matching
4cefb3f4
adomani fix alternating_group
6d38b3dd
adomani fix 4squares
d51810ab
adomani fix numberfield
0f727f25
adomani fix cyclo eval
6b58781d
adomani fix 45partition
b019e942
adomani fix 2013_q1
fe6ddec6
adomani fix convex specific functions
f15e0496
adomani typo
8deb8844
adomani really fix specific_functions
de34699e
adomani fix perfect numbers
efc598ac
adomani remove check
db0d2fb3
adomani not.trans
a70bed04
adomani golf
35738b83
khwilson feat(algebra/square): Add the notion of "square" elements of monoids
1b687f3c
khwilson Linting
e417f956
khwilson More linting
10be7082
khwilson Update src/algebra/square.lean
97a502ed
khwilson Update src/algebra/square.lean
38e5a5c0
khwilson Update src/algebra/square.lean
8c91e102
khwilson Extraneous end
6981f42e
khwilson Split out square_mul into sublemmas
311ee718
khwilson Further golfing
bc2483af
khwilson Further PR requests
082364b8
khwilson Rebasing on #13037
e1008156
khwilson
khwilson khwilson added blocked-by-other-PR
leanprover-community-bot-assistant leanprover-community-bot-assistant removed blocked-by-other-PR
adomani
khwilson Moving everything to new homes based on rebased commit
2dd80088
khwilson Move sqrt0 to nat
fc54eb8c
khwilson Merge branch 'master' into add_square
47f5cde8
khwilson Finish merge
add0565a
khwilson Merge branch 'add_square' of https://github.com/leanprover-community/…
6cd1e179
khwilson Remove square file
c31b35ee
khwilson Fix docstring location
0f9fd657
khwilson
khwilson Fix a mismerge
c119331d
adomani
adomani
adomani commented on 2022-04-06
khwilson Update src/algebra/parity.lean
5d56d04e
YaelDillies
YaelDillies commented on 2022-04-10
khwilson Update src/algebra/parity.lean
c82de51c
khwilson yaels comments
e6e71ddd
khwilson
khwilson
leanprover-community-bot-assistant leanprover-community-bot-assistant added merge-conflict
khwilson Remove sqrt0
d56743c4
khwilson
leanprover-community-bot-assistant leanprover-community-bot-assistant removed merge-conflict
khwilson Merge branch 'master' into add_square
d0994b4c
khwilson Final comments plus some simp issues
46b16fd8
khwilson
YaelDillies YaelDillies changed the title feat(algebra/square): Add the notion of "square" elements of monoids feat(algebra/parity): Squares and primality 3 years ago
YaelDillies
YaelDillies commented on 2022-04-15
khwilson yaels comments
1c5878e9
khwilson
YaelDillies
YaelDillies commented on 2022-04-18
khwilson unindent after trivial goal
6ca0abae
jcommelin
jcommelin commented on 2022-04-21
jcommelin jcommelin removed awaiting-review
jcommelin jcommelin added awaiting-author
khwilson khwilson removed awaiting-author
khwilson khwilson added awaiting-review
khwilson Change name of lemma
3aca6c64
YaelDillies
YaelDillies commented on 2022-04-21
khwilson Update src/data/nat/factorization.lean
723f4ca9
khwilson Update src/data/nat/factorization.lean
9a1d7b76
leanprover-community-bot-assistant leanprover-community-bot-assistant added merge-conflict
khwilson Merge branch 'master' into add_square
d49aa14c
leanprover-community-bot-assistant leanprover-community-bot-assistant removed merge-conflict
khwilson Update parity.lean
18b025f6
khwilson Removed simps
ee720bf3
khwilson
khwilson Fix unrelated file
f7d0e2de
khwilson Merge branch 'master' into add_square
ff263277
khwilson
YaelDillies Merge remote-tracking branch 'origin/master' into add_square
5f4938ac
YaelDillies
YaelDillies fix
c6941519
YaelDillies move nat.cast_apply
6cf566a7
YaelDillies revert imports
d87bc3f8
mathlib-dependent-issues-bot mathlib-dependent-issues-bot added blocked-by-other-PR
khwilson
YaelDillies
khwilson
mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed blocked-by-other-PR
mathlib-dependent-issues-bot
YaelDillies Merge remote-tracking branch 'origin/master' into add_square
44d3e465
jcommelin
jcommelin jcommelin removed awaiting-review
jcommelin jcommelin added awaiting-author
kim-em kim-em added too-late

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
awaiting-author too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum