Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-02 17:42 5cbd7fa7

View on Github →

changing names

Estimated changes

Modified src/data/gaussian_int.lean

deleted theorem gaussian_int.int_cast_im

deleted theorem gaussian_int.int_cast_re

deleted theorem gaussian_int.to_complex_im'

added theorem gaussian_int.to_complex_im

deleted theorem gaussian_int.to_complex_re'

added theorem gaussian_int.to_complex_re

added theorem gaussian_int.to_real_im

added theorem gaussian_int.to_real_re

Modified src/data/zmod/quadratic_reciprocity.lean

added theorem zmodp.exists_pow_two_eq_neg_one_iff_mod_four_ne_three

added theorem zmodp.exists_pow_two_eq_prime_iff_of_mod_four_eq_one

added theorem zmodp.exists_pow_two_eq_prime_iff_of_mod_four_eq_three

deleted theorem zmodp.is_square_iff_is_not_square_of_mod_four_eq_three

deleted theorem zmodp.is_square_iff_is_square_of_mod_four_eq_one

deleted theorem zmodp.neg_one_is_square_iff_mod_four_ne_three