mathlib3
c36470f7 - put sum_two_squares in nat.prime namespace

Commit

7 years ago

put sum_two_squares in nat.prime namespace

References

#776 - feat(number_theory/sum_two_squares): fermat's theorem on sums of two squares

Author

ChrisHughes24

ChrisHughes24

Committer

avigad

avigad

Parents

Loading