mathlib3
feat(number_theory/sum_two_squares): fermat's theorem on sums of two squares
#776
Merged
Merged
feat(number_theory/sum_two_squares): fermat's theorem on sums of two squares #776
avigad
merged
23 commits into
master
from
sum_two_squares
prove Z[i] is a euclidean_domain
9b96b347
commit properly
c81f79fe
Merge remote-tracking branch 'comm/master'
4137ea71
Merge remote-tracking branch 'comm/master'
c49b99fe
finish proof of sum two squares
81d1676b
Merge remote-tracking branch 'comm/master'
d8dfe7aa
fix build
7ee092f5
move lemmas to correct places
7cfd81ca
put sum_two_squares in nat.prime namespace
fc11cc37
Merge branch 'master' into sum_two_squares
1d6b1345
The year is 2019
61fb8d4c
Merge branch 'sum_two_squares' of https://github.com/leanprover-commu…
06760e2f
Merge branch 'master' of https://github.com/leanprover-community/math…
c44d602c
Merge remote-tracking branch 'comm/master' into sum_two_squares
554daa79
changing names
f17730a0
fix build
949bb838
generalize norm to zsqrtd
79bb51c3
Merge branch 'master' into sum_two_squares
e02b31d3
fix build
ffd0d53d
fix build
c666dc78
fix properly
8ddf2e1d
Merge remote-tracking branch 'comm/master' into sum_two_squares
a937d5df
hopefully fixed for good this time
20a2af00
Login to write a write a comment.
Login via GitHub