Mathlib v3 is deprecated. Go to Mathlib v4

Theorem zmodp.neg_one_is_square_iff_mod_four_ne_three

Modification history

2019-03-02 17:42
src/data/zmod/quadratic_reciprocity.lean
changing names
Deleted zmodp.neg_one_is_square_iff_mod_four_ne_threeView on Github →
2019-03-02 17:42
src/data/zmod/quadratic_reciprocity.lean
commit properly
Added zmodp.neg_one_is_square_iff_mod_four_ne_threeView on Github →