Commit 2019-11-10 19:42 f738ec7e
View on Github →refactor(data/zmod/quadratic_reciprocity): simplify proof of quadratic reciprocity and prove when 2 is a square (#1609)
- feat(number_theory/sum_four_squares): every natural number is the sum of four square numbers
- gauss_lemma
- Johan's suggestions
- some better parity proofs
- refactor(data/finset): restate disjoint_filter
- fix build
- fix silly lemmas in finite_fields
- generalize a lemma
- work on add_sum_mul_div_eq_mul
- fix build
- Update src/number_theory/sum_four_squares.lean
- feat(data/multiset): map_eq_map_of_bij_of_nodup
- finish proof of quad_rec
- minor fix
- Add docs
- add docs in correct style
- Use Ico 1 p instead of (range p).erase 0