mathlib3
e72f275d - feat(number_theory/qudratic_reciprocity): change type of `a` in API lemmas to `int` (#13393)

Commit
3 years ago
feat(number_theory/qudratic_reciprocity): change type of `a` in API lemmas to `int` (#13393) This is step 2 in the overhaul of number_theory/qudratic_reciprocity. The only changes are that the argument `a` is now of type `int` rather than `nat` in a bunch of statements. This is more natural, since the corresponding (now second) argument of `legendre_symnbol` is of type `int`; it therefore makes the API lemmas more easily useable.
Parents
Loading