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