Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-02 17:42 d8f0921a

View on Github →

move lemmas to correct places

Estimated changes

Created src/data/gaussian_int.lean

added theorem gaussian_int.div_def

added theorem gaussian_int.int_cast_im

added theorem gaussian_int.int_cast_re

added theorem gaussian_int.mod_def

added theorem gaussian_int.nat_cast_complex_norm

added theorem gaussian_int.nat_cast_real_norm

added def gaussian_int.norm

added theorem gaussian_int.norm_eq_one_iff

added theorem gaussian_int.norm_eq_zero

added theorem gaussian_int.norm_le_norm_mul_left

added theorem gaussian_int.norm_mul

added theorem gaussian_int.norm_nat_cast

added theorem gaussian_int.norm_one

added theorem gaussian_int.norm_pos

added theorem gaussian_int.norm_sq_div_sub_div_lt_one

added theorem gaussian_int.norm_sq_le_norm_sq_of_re_le_of_im_le

added theorem gaussian_int.norm_zero

added def gaussian_int.to_complex

added theorem gaussian_int.to_complex_add

added theorem gaussian_int.to_complex_def'

added theorem gaussian_int.to_complex_def

added theorem gaussian_int.to_complex_def₂

added theorem gaussian_int.to_complex_div_im

added theorem gaussian_int.to_complex_div_re

added theorem gaussian_int.to_complex_eq_zero

added theorem gaussian_int.to_complex_im'

added theorem gaussian_int.to_complex_inj

added theorem gaussian_int.to_complex_mul

added theorem gaussian_int.to_complex_neg

added theorem gaussian_int.to_complex_one

added theorem gaussian_int.to_complex_re'

added theorem gaussian_int.to_complex_sub

added theorem gaussian_int.to_complex_zero

added def gaussian_int

Modified src/number_theory/sum_two_squares.lean

deleted theorem gaussian_int.div_def

deleted theorem gaussian_int.int_cast_im

deleted theorem gaussian_int.int_cast_re

deleted theorem gaussian_int.mod_def

deleted theorem gaussian_int.nat_cast_complex_norm

deleted theorem gaussian_int.nat_cast_real_norm

deleted def gaussian_int.norm

deleted theorem gaussian_int.norm_eq_one_iff

deleted theorem gaussian_int.norm_eq_zero

deleted theorem gaussian_int.norm_le_norm_mul_left

deleted theorem gaussian_int.norm_mul

deleted theorem gaussian_int.norm_nat_cast

deleted theorem gaussian_int.norm_one

deleted theorem gaussian_int.norm_pos

deleted theorem gaussian_int.norm_sq_div_sub_div_lt_one

deleted theorem gaussian_int.norm_sq_le_norm_sq_of_re_le_of_im_le

deleted theorem gaussian_int.norm_zero

deleted def gaussian_int.to_complex

deleted theorem gaussian_int.to_complex_add

deleted theorem gaussian_int.to_complex_def'

deleted theorem gaussian_int.to_complex_def

deleted theorem gaussian_int.to_complex_def₂

deleted theorem gaussian_int.to_complex_div_im

deleted theorem gaussian_int.to_complex_div_re

deleted theorem gaussian_int.to_complex_eq_zero

deleted theorem gaussian_int.to_complex_im'

deleted theorem gaussian_int.to_complex_inj

deleted theorem gaussian_int.to_complex_mul

deleted theorem gaussian_int.to_complex_neg

deleted theorem gaussian_int.to_complex_one

deleted theorem gaussian_int.to_complex_re'

deleted theorem gaussian_int.to_complex_sub

deleted theorem gaussian_int.to_complex_zero

deleted def gaussian_int