Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-29 23:56 c2bb4c5c

View on Github →

refactor(data/zsqrtd/basic): move zsqrtd out of pell and into data (#861)

Estimated changes

added def zsqrtd.add
added theorem zsqrtd.add_def
added theorem zsqrtd.add_im
added theorem zsqrtd.add_re
added theorem zsqrtd.bit0_im
added theorem zsqrtd.bit0_re
added theorem zsqrtd.bit1_im
added theorem zsqrtd.bit1_re
added theorem zsqrtd.coe_int_im
added theorem zsqrtd.coe_int_re
added theorem zsqrtd.coe_int_val
added theorem zsqrtd.coe_nat_im
added theorem zsqrtd.coe_nat_re
added theorem zsqrtd.coe_nat_val
added def zsqrtd.conj
added theorem zsqrtd.conj_im
added theorem zsqrtd.conj_mul
added theorem zsqrtd.conj_re
added theorem zsqrtd.d_pos
added theorem zsqrtd.decompose
added theorem zsqrtd.ext
added theorem zsqrtd.le_antisymm
added theorem zsqrtd.le_arch
added theorem zsqrtd.le_of_le_le
added theorem zsqrtd.le_refl
added def zsqrtd.mul
added theorem zsqrtd.mul_conj
added theorem zsqrtd.mul_im
added theorem zsqrtd.mul_re
added theorem zsqrtd.muld_val
added def zsqrtd.neg
added theorem zsqrtd.neg_im
added theorem zsqrtd.neg_re
added def zsqrtd.nonneg
added theorem zsqrtd.nonneg_add
added theorem zsqrtd.nonneg_add_lem
added theorem zsqrtd.nonneg_antisymm
added theorem zsqrtd.nonneg_cases
added theorem zsqrtd.nonneg_mul
added theorem zsqrtd.nonneg_mul_lem
added theorem zsqrtd.nonneg_muld
added theorem zsqrtd.nonneg_smul
added def zsqrtd.nonnegg
added theorem zsqrtd.nonnegg_comm
added theorem zsqrtd.nonnegg_neg_pos
added theorem zsqrtd.nonnegg_pos_neg
added def zsqrtd.norm
added theorem zsqrtd.norm_eq_one_iff
added theorem zsqrtd.norm_int_cast
added theorem zsqrtd.norm_mul
added theorem zsqrtd.norm_nat_cast
added theorem zsqrtd.norm_nonneg
added theorem zsqrtd.norm_one
added theorem zsqrtd.norm_zero
added theorem zsqrtd.not_sq_le_succ
added def zsqrtd.of_int
added theorem zsqrtd.of_int_eq_coe
added theorem zsqrtd.of_int_im
added theorem zsqrtd.of_int_re
added def zsqrtd.one
added theorem zsqrtd.one_im
added theorem zsqrtd.one_re
added theorem zsqrtd.smul_val
added theorem zsqrtd.smuld_val
added def zsqrtd.sq_le
added theorem zsqrtd.sq_le_add
added theorem zsqrtd.sq_le_add_mixed
added theorem zsqrtd.sq_le_cancel
added theorem zsqrtd.sq_le_mul
added theorem zsqrtd.sq_le_of_le
added theorem zsqrtd.sq_le_smul
added def zsqrtd.sqrtd
added theorem zsqrtd.sqrtd_im
added theorem zsqrtd.sqrtd_re
added def zsqrtd.zero
added theorem zsqrtd.zero_im
added theorem zsqrtd.zero_re
added structure zsqrtd
deleted def zsqrtd.add
deleted theorem zsqrtd.add_def
deleted theorem zsqrtd.add_im
deleted theorem zsqrtd.add_re
deleted theorem zsqrtd.bit0_im
deleted theorem zsqrtd.bit0_re
deleted theorem zsqrtd.bit1_im
deleted theorem zsqrtd.bit1_re
deleted theorem zsqrtd.coe_int_im
deleted theorem zsqrtd.coe_int_re
deleted theorem zsqrtd.coe_int_val
deleted theorem zsqrtd.coe_nat_im
deleted theorem zsqrtd.coe_nat_re
deleted theorem zsqrtd.coe_nat_val
deleted def zsqrtd.conj
deleted theorem zsqrtd.conj_im
deleted theorem zsqrtd.conj_mul
deleted theorem zsqrtd.conj_re
deleted theorem zsqrtd.d_pos
deleted theorem zsqrtd.decompose
deleted theorem zsqrtd.divides_sq_eq_zero
deleted theorem zsqrtd.ext
deleted theorem zsqrtd.le_antisymm
deleted theorem zsqrtd.le_arch
deleted theorem zsqrtd.le_of_le_le
deleted theorem zsqrtd.le_refl
deleted def zsqrtd.mul
deleted theorem zsqrtd.mul_conj
deleted theorem zsqrtd.mul_im
deleted theorem zsqrtd.mul_re
deleted theorem zsqrtd.muld_val
deleted def zsqrtd.neg
deleted theorem zsqrtd.neg_im
deleted theorem zsqrtd.neg_re
deleted def zsqrtd.nonneg
deleted theorem zsqrtd.nonneg_add
deleted theorem zsqrtd.nonneg_add_lem
deleted theorem zsqrtd.nonneg_antisymm
deleted theorem zsqrtd.nonneg_cases
deleted theorem zsqrtd.nonneg_iff_zero_le
deleted theorem zsqrtd.nonneg_mul
deleted theorem zsqrtd.nonneg_mul_lem
deleted theorem zsqrtd.nonneg_muld
deleted theorem zsqrtd.nonneg_smul
deleted def zsqrtd.nonnegg
deleted theorem zsqrtd.nonnegg_cases_left
deleted theorem zsqrtd.nonnegg_comm
deleted theorem zsqrtd.nonnegg_neg_pos
deleted theorem zsqrtd.nonnegg_pos_neg
deleted def zsqrtd.norm
deleted theorem zsqrtd.norm_eq_mul_conj
deleted theorem zsqrtd.norm_eq_one_iff
deleted theorem zsqrtd.norm_int_cast
deleted theorem zsqrtd.norm_mul
deleted theorem zsqrtd.norm_nat_cast
deleted theorem zsqrtd.norm_nonneg
deleted theorem zsqrtd.norm_one
deleted theorem zsqrtd.norm_zero
deleted theorem zsqrtd.not_divides_square
deleted theorem zsqrtd.not_sq_le_succ
deleted def zsqrtd.of_int
deleted theorem zsqrtd.of_int_eq_coe
deleted theorem zsqrtd.of_int_im
deleted theorem zsqrtd.of_int_re
deleted def zsqrtd.one
deleted theorem zsqrtd.one_im
deleted theorem zsqrtd.one_re
deleted theorem zsqrtd.smul_val
deleted theorem zsqrtd.smuld_val
deleted def zsqrtd.sq_le
deleted theorem zsqrtd.sq_le_add
deleted theorem zsqrtd.sq_le_add_mixed
deleted theorem zsqrtd.sq_le_cancel
deleted theorem zsqrtd.sq_le_mul
deleted theorem zsqrtd.sq_le_of_le
deleted theorem zsqrtd.sq_le_smul
deleted def zsqrtd.sqrtd
deleted theorem zsqrtd.sqrtd_im
deleted theorem zsqrtd.sqrtd_re
deleted def zsqrtd.zero
deleted theorem zsqrtd.zero_im
deleted theorem zsqrtd.zero_re
deleted structure zsqrtd