Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-02 17:42 49a85f48

View on Github →

prove Z[i] is a euclidean_domain

Estimated changes

Modified src/algebra/archimedean.lean

added theorem abs_sub_round

added theorem rat.cast_round

added def round

Created src/number_theory/sum_two_squares.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_zero

added theorem gaussian_int.norm_mul

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 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