Mathlib Changelog
v3
Changelog
About
Github
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
Modified
algebra/archimedean.lean
added
theorem
ceil_nonneg
added
theorem
ceil_pos
Created
algebra/field_power.lean
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_ne_zero_of_ne_zero
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
Modified
algebra/order_functions.lean
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_le_add_of_nonneg_left
added
theorem
min_le_add_of_nonneg_right
added
theorem
min_sub
Modified
algebra/ordered_field.lean
added
theorem
inv_le_one
Modified
algebra/ordered_ring.lean
added
theorem
mul_le_one
Modified
data/int/basic.lean
added
theorem
int.dvd_nat_abs_of_of_nat_dvd
added
theorem
int.eq_mul_div_of_mul_eq_mul_of_dvd_left
added
theorem
int.nat_abs_ne_zero_of_ne_zero
added
theorem
int.of_nat_dvd_of_dvd_nat_abs
added
theorem
int.pow_div_of_le_of_pow_div_int
Modified
data/nat/basic.lean
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.nat.find_greatest_is_greatest
added
theorem
nat.nat.find_greatest_spec
added
theorem
nat.not_pos_pow_dvd
added
theorem
nat.one_pow
added
theorem
nat.pow_div_of_le_of_pow_div
added
theorem
nat.pow_eq_mul_pow_sub
added
theorem
nat.pow_lt_pow_succ
added
theorem
nat.pow_pos
Modified
data/nat/prime.lean
added
theorem
nat.prime.ne_zero
added
theorem
nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul
added
theorem
nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul_int
Created
data/padics/padic_integers.lean
added
def
padic_int.add
added
def
padic_int.mul
added
def
padic_int.neg
added
def
padic_int
Created
data/padics/padic_norm.lean
added
theorem
padic_norm.add_eq_max_of_ne
added
theorem
padic_norm.triangle_ineq
added
theorem
padic_norm.zero_of_padic_norm_eq_zero
added
def
padic_norm
added
theorem
padic_val.is_greatest
added
theorem
padic_val.le_padic_val_of_pow_div
added
theorem
padic_val.min_le_padic_val_add
added
theorem
padic_val.padic_val_self
added
theorem
padic_val.spec
added
theorem
padic_val.unique
added
def
padic_val
added
theorem
padic_val_rat.min_le_padic_val_rat_add
added
theorem
padic_val_rat.padic_val_rat_self
added
def
padic_val_rat
Created
data/padics/padic_rationals.lean
added
theorem
padic.cast_eq_of_rat
added
theorem
padic.cast_eq_of_rat_of_int
added
theorem
padic.cast_eq_of_rat_of_nat
added
theorem
padic.complete
added
theorem
padic.const_equiv
added
theorem
padic.exi_rat_seq_conv
added
theorem
padic.exi_rat_seq_conv_cauchy
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.eq_padic_norm
added
theorem
padic_norm_e.nonarchimedean
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
theorem
padic_seq.eq_zero_iff_equiv_zero
added
theorem
padic_seq.equiv_zero_of_val_eq_of_equiv_zero
added
theorem
padic_seq.ne_zero_iff_nequiv_zero
added
def
padic_seq.norm
added
theorem
padic_seq.norm_const
added
theorem
padic_seq.norm_eq
added
theorem
padic_seq.norm_eq_norm_app_of_nonzero
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_nonarchimedean
added
theorem
padic_seq.norm_nonneg
added
theorem
padic_seq.norm_nonzero_of_not_equiv_zero
added
theorem
padic_seq.norm_one
added
theorem
padic_seq.norm_zero_iff
added
theorem
padic_seq.not_equiv_zero_const_of_nonzero
added
theorem
padic_seq.not_lim_zero_const_of_nonzero
added
theorem
padic_seq.stationary
added
def
padic_seq.stationary_point
added
theorem
padic_seq.stationary_point_spec
added
def
padic_seq
Modified
data/rat.lean
added
theorem
rat.denom_ne_zero
added
theorem
rat.denom_neg_eq_denom
added
theorem
rat.mk_denom_ne_zero_of_ne_zero
added
theorem
rat.mk_ne_zero_of_ne_zero
added
theorem
rat.mk_num_ne_zero_of_ne_zero
added
theorem
rat.mul_num_denom
added
theorem
rat.num_denom_mk
modified
theorem
rat.num_dvd
added
theorem
rat.num_ne_zero_of_ne_zero
added
theorem
rat.num_neg_eq_neg_num
added
theorem
rat.num_zero
added
theorem
rat.zero_of_num_zero
Modified
data/real/basic.lean
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
Modified
data/real/cau_seq.lean
added
theorem
cau_seq.mul_equiv_zero'
added
theorem
cau_seq.mul_equiv_zero
added
theorem
cau_seq.mul_not_equiv_zero
added
theorem
cau_seq.not_lim_zero_of_not_congr_zero
added
theorem
cau_seq.one_not_equiv_zero
Created
data/real/cau_seq_completion.lean
added
def
cau_seq.completion.Cauchy
added
theorem
cau_seq.completion.cau_seq_zero_ne_one
added
theorem
cau_seq.completion.inv_mk
added
theorem
cau_seq.completion.inv_zero
added
def
cau_seq.completion.mk
added
theorem
cau_seq.completion.mk_add
added
theorem
cau_seq.completion.mk_eq
added
theorem
cau_seq.completion.mk_eq_mk
added
theorem
cau_seq.completion.mk_eq_zero
added
theorem
cau_seq.completion.mk_mul
added
theorem
cau_seq.completion.mk_neg
added
def
cau_seq.completion.of_rat
added
theorem
cau_seq.completion.of_rat_add
added
theorem
cau_seq.completion.of_rat_div
added
theorem
cau_seq.completion.of_rat_inv
added
theorem
cau_seq.completion.of_rat_mul
added
theorem
cau_seq.completion.of_rat_neg
added
theorem
cau_seq.completion.of_rat_one
added
theorem
cau_seq.completion.of_rat_sub
added
theorem
cau_seq.completion.of_rat_zero
added
theorem
cau_seq.completion.zero_ne_one