Mathlib Changelog
v3
Changelog
About
Github
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
Created
src/data/zsqrtd/basic.lean
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.divides_sq_eq_zero
added
theorem
zsqrtd.divides_sq_eq_zero_z
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_iff_zero_le
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_cases_left
added
theorem
zsqrtd.nonnegg_cases_right
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_mul_conj
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_divides_square
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
Renamed
src/data/gaussian_int.lean
to
src/data/zsqrtd/gaussian_int.lean
Modified
src/number_theory/pell.lean
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.divides_sq_eq_zero_z
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_cases_right
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
Modified
src/number_theory/sum_two_squares.lean