Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-16 11:23 93817f17

View on Github →

feat(data/padics): p-adic numbers (#262)

Estimated changes

added theorem ceil_nonneg
added theorem ceil_pos
added def fpow
added theorem fpow_add
added theorem fpow_eq_gpow
added theorem fpow_inv
added theorem fpow_le_of_le
added theorem fpow_nonneg_of_nonneg
added theorem fpow_zero
added theorem pow_le_max_of_min_le
added theorem unit_pow
added theorem zero_fpow
added theorem zero_gpow
added theorem le_of_max_le_left
added theorem le_of_max_le_right
added theorem max_le_add_of_nonneg
added theorem min_add
added theorem min_sub
added theorem inv_le_one
added theorem mul_le_one
added theorem nat.dvd_div_of_mul_dvd
added theorem nat.lt_pow_self
added theorem nat.mul_dvd_of_dvd_div
added theorem nat.nat.div_mul_div
added theorem nat.not_pos_pow_dvd
added theorem nat.one_pow
added theorem nat.pow_eq_mul_pow_sub
added theorem nat.pow_lt_pow_succ
added theorem nat.pow_pos
added theorem nat.prime.ne_zero
added def padic_int.add
added def padic_int.mul
added def padic_int.neg
added def padic_int
added def padic_norm
added theorem padic_val.is_greatest
added theorem padic_val.spec
added theorem padic_val.unique
added def padic_val
added def padic_val_rat
added theorem padic.cast_eq_of_rat
added theorem padic.complete
added theorem padic.const_equiv
added theorem padic.exi_rat_seq_conv
added def padic.lim_seq
added def padic.mk
added theorem padic.mk_eq
added def padic.of_rat
added theorem padic.of_rat_add
added theorem padic.of_rat_div
added theorem padic.of_rat_eq
added theorem padic.of_rat_mul
added theorem padic.of_rat_neg
added theorem padic.of_rat_one
added theorem padic.of_rat_sub
added theorem padic.of_rat_zero
added theorem padic.rat_dense
added def padic
added theorem padic_norm_e.defn
added theorem padic_norm_e.sub_rev
added theorem padic_norm_e.zero_def
added theorem padic_norm_e.zero_iff
added def padic_norm_e
added def padic_seq.norm
added theorem padic_seq.norm_const
added theorem padic_seq.norm_eq
added theorem padic_seq.norm_equiv
added theorem padic_seq.norm_image
added theorem padic_seq.norm_mul
added theorem padic_seq.norm_neg
added theorem padic_seq.norm_nonneg
added theorem padic_seq.norm_one
added theorem padic_seq.stationary
added def padic_seq
added theorem rat.denom_ne_zero
added theorem rat.denom_neg_eq_denom
added theorem rat.mul_num_denom
added theorem rat.num_denom_mk
modified theorem rat.num_dvd
added theorem rat.num_neg_eq_neg_num
added theorem rat.num_zero
added theorem rat.zero_of_num_zero
deleted theorem real.inv_mk
deleted theorem real.inv_zero
deleted def real.mk
deleted theorem real.mk_add
deleted theorem real.mk_eq
deleted theorem real.mk_eq_mk
deleted theorem real.mk_eq_zero
deleted theorem real.mk_mul
deleted theorem real.mk_neg
modified def real.of_rat
deleted theorem real.of_rat_add
deleted theorem real.of_rat_mul
deleted theorem real.of_rat_neg
deleted theorem real.of_rat_one
deleted theorem real.of_rat_zero
modified def real
added theorem cau_seq.mul_equiv_zero