Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2018-01-26 02:52
f46d32b0
View on Github →
feat(algebra/archimedean): generalize real thms to archimedean fields
Estimated changes
Created
algebra/archimedean.lean
added
theorem
archimedean_iff_nat_le
added
theorem
archimedean_iff_nat_lt
added
theorem
archimedean_iff_rat_le
added
theorem
archimedean_iff_rat_lt
added
def
ceil
added
theorem
ceil_add_int
added
theorem
ceil_coe
added
theorem
ceil_le
added
theorem
ceil_lt_add_one
added
theorem
ceil_mono
added
theorem
ceil_sub_int
added
theorem
exists_floor
added
theorem
exists_int_gt
added
theorem
exists_int_lt
added
theorem
exists_nat_gt
added
theorem
exists_pos_rat_lt
added
theorem
exists_rat_btwn
added
theorem
exists_rat_gt
added
theorem
exists_rat_lt
added
theorem
exists_rat_near
added
def
floor
added
theorem
floor_add_int
added
theorem
floor_coe
added
theorem
floor_le
added
theorem
floor_lt
added
theorem
floor_mono
added
theorem
floor_nonneg
added
theorem
floor_sub_int
added
theorem
le_ceil
added
theorem
le_floor
added
theorem
lt_ceil
added
theorem
lt_floor_add_one
added
theorem
lt_succ_floor
added
theorem
sub_one_lt_floor
Modified
algebra/group_power.lean
added
theorem
add_monoid.mul_smul_assoc
added
theorem
add_monoid.mul_smul_right
added
theorem
add_monoid.one_smul
added
theorem
add_monoid.smul_eq_mul'
added
theorem
add_monoid.smul_eq_mul
added
theorem
add_monoid.smul_nonneg
added
theorem
gsmul_eq_mul'
added
theorem
gsmul_eq_mul
added
theorem
mul_gsmul_assoc
added
theorem
mul_gsmul_right
added
theorem
one_le_pow_of_one_le
added
theorem
pow_ge_one_add_mul
added
theorem
pow_ge_one_add_sub_mul
deleted
theorem
pow_ge_one_of_ge_one
modified
theorem
pow_nonneg
modified
theorem
pow_pos
Modified
analysis/complex.lean
Modified
analysis/ennreal.lean
Modified
analysis/limits.lean
Modified
analysis/measure_theory/borel_space.lean
Modified
analysis/measure_theory/lebesgue_measure.lean
Modified
analysis/real.lean
Renamed
data/complex.lean
to
data/complex/basic.lean
added
theorem
complex.abs_le_abs_re_add_abs_im
added
theorem
complex.equiv_lim
added
theorem
complex.is_cau_seq_im
added
theorem
complex.is_cau_seq_re
added
theorem
complex.re_add_im
Modified
data/rat.lean
added
theorem
rat.coe_int_denom
added
theorem
rat.coe_int_num
added
theorem
rat.coe_nat_denom
added
theorem
rat.coe_nat_num
Modified
data/real/basic.lean
deleted
theorem
real.ceil_add_int
deleted
theorem
real.ceil_coe
deleted
theorem
real.ceil_le
deleted
theorem
real.ceil_lt_add_one
deleted
theorem
real.ceil_mono
deleted
theorem
real.ceil_sub_int
deleted
theorem
real.exists_int_gt
deleted
theorem
real.exists_int_lt
deleted
theorem
real.exists_nat_gt
deleted
theorem
real.exists_pos_rat_lt
deleted
theorem
real.exists_rat_btwn
deleted
theorem
real.exists_rat_gt
deleted
theorem
real.exists_rat_lt
deleted
theorem
real.exists_rat_near'
deleted
theorem
real.exists_rat_near
deleted
theorem
real.floor_add_int
deleted
theorem
real.floor_coe
deleted
theorem
real.floor_le
deleted
theorem
real.floor_lt
deleted
theorem
real.floor_mono
deleted
theorem
real.floor_nonneg
deleted
theorem
real.floor_sub_int
deleted
theorem
real.le_ceil
deleted
theorem
real.le_floor
modified
theorem
real.le_mk_of_forall_le
deleted
theorem
real.lt_ceil
deleted
theorem
real.lt_floor_add_one
deleted
theorem
real.lt_succ_floor
modified
theorem
real.mk_le_of_forall_le
modified
theorem
real.mk_near_of_forall_near
deleted
theorem
real.sub_one_lt_floor
Modified
data/real/cau_seq.lean
added
theorem
cau_seq.is_cau
added
theorem
cau_seq.mk_to_fun
Modified
set_theory/ordinal_notation.lean