Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-10-24 22:31 dd9f766f

View on Github →

feat(data/num,data/nat/cast,...): nat,num,int,rat.cast, list stuff

Estimated changes

Modified algebra/field.lean

added theorem inv_comm_of_comm

Modified algebra/group.lean

added theorem eq_inv_iff_mul_eq_one

modified theorem eq_inv_mul_iff_mul_eq

modified theorem eq_mul_inv_iff_mul_eq

modified theorem eq_sub_iff_add_eq

added theorem inv_eq_iff_mul_eq_one

modified theorem inv_mul_eq_iff_eq_mul

modified theorem mul_inv_eq_iff_eq_mul

Modified algebra/group_power.lean

added theorem nat.pow_eq_pow_nat

Modified algebra/ordered_ring.lean

added theorem mul_nonneg_iff_right_nonneg_of_pos

Modified analysis/limits.lean

modified theorem mul_add_one_le_pow

Modified analysis/measure_theory/lebesgue_measure.lean

modified theorem measure_theory.tendsto_of_nat_at_top_at_top

Modified analysis/metric_space.lean

Deleted analysis/of_nat.lean

deleted theorem exists_lt_of_nat

deleted theorem int_of_nat_eq_of_nat

deleted def of_nat

deleted theorem of_nat_add

deleted theorem of_nat_bit0

deleted theorem of_nat_bit1

deleted theorem of_nat_le_of_nat

deleted theorem of_nat_le_of_nat_iff

deleted theorem of_nat_mul

deleted theorem of_nat_one

deleted theorem of_nat_pos

deleted theorem of_nat_sub

deleted theorem rat_coe_eq_of_nat

deleted theorem rat_of_nat_eq_of_nat

deleted theorem real_of_rat_of_nat_eq_of_nat

deleted theorem zero_le_of_nat

Modified analysis/real.lean

added theorem coe_rat_eq_of_rat

added theorem exists_lt_nat

modified def lift_rat_fun

modified def lift_rat_op

Modified data/encodable.lean

modified def encodable_of_equiv

Modified data/equiv.lean

added theorem equiv.apply_inverse_apply

added def equiv.int_equiv_nat

added def equiv.int_equiv_nat_sum_nat

added def equiv.psigma_equiv_sigma

added def equiv.psum_equiv_sum

added def equiv.sigma_congr_left

added def equiv.sigma_congr_right

added def equiv.sigma_equiv_prod

added def equiv.sigma_equiv_prod_of_equiv

Modified data/finset/basic.lean

Modified data/int/basic.lean

added theorem int.cast_add

added theorem int.cast_bit0

added theorem int.cast_bit1

added theorem int.cast_coe_nat

added theorem int.cast_eq_zero

added theorem int.cast_id

added theorem int.cast_inj

added theorem int.cast_le

added theorem int.cast_lt

added theorem int.cast_lt_zero

added theorem int.cast_mul

added theorem int.cast_ne_zero

added theorem int.cast_neg

added theorem int.cast_neg_of_nat

added theorem int.cast_neg_succ_of_nat

added theorem int.cast_nonneg

added theorem int.cast_nonpos

added theorem int.cast_of_nat

added theorem int.cast_one

added theorem int.cast_pos

added theorem int.cast_sub

added theorem int.cast_sub_nat_nat

added theorem int.cast_zero

added theorem int.coe_nat_dvd

deleted theorem int.coe_nat_dvd_coe_nat_iff

deleted theorem int.coe_nat_dvd_coe_nat_of_dvd

deleted theorem int.coe_nat_dvd_left

deleted theorem int.coe_nat_dvd_right

added theorem int.coe_nat_eq_zero

added theorem int.coe_nat_inj'

added theorem int.coe_nat_le

added theorem int.coe_nat_lt

added theorem int.coe_nat_ne_zero

added theorem int.coe_nat_pos

added theorem int.dvd_nat_abs

deleted theorem int.dvd_of_coe_nat_dvd_coe_nat

added theorem int.mul_cast_comm

added theorem int.nat_abs_dvd

added theorem int.nat_cast_eq_coe_nat

Modified data/list/basic.lean

added theorem list.diff_cons

added theorem list.diff_eq_foldl

added theorem list.diff_nil

added theorem list.erase_comm

Modified data/list/perm.lean

added theorem list.count_le_of_subperm

added theorem list.countp_le_of_subperm

added theorem list.exists_perm_append_of_sublist

deleted theorem list.exists_sublist_perm_of_subset_nodup

added theorem list.length_le_of_subperm

deleted theorem list.mem_iff_mem_of_perm

modified theorem list.mem_of_perm

added theorem list.perm.subperm_left

added theorem list.perm.subperm_right

deleted theorem list.perm_app_inv_right

added theorem list.perm_app_right_iff

added theorem list.perm_diff_left

added theorem list.perm_diff_right

added theorem list.perm_subset

added theorem list.subperm.antisymm

added theorem list.subperm.exists_of_length_lt

added theorem list.subperm.perm_of_length_le

added theorem list.subperm.refl

added theorem list.subperm.trans

added def list.subperm

added theorem list.subperm_app_left

added theorem list.subperm_app_right

added theorem list.subperm_cons

added theorem list.subperm_of_perm

added theorem list.subperm_of_sublist

added theorem list.subperm_of_subset_nodup

added theorem list.subset_of_subperm

Modified data/list/sort.lean

Created data/nat/cast.lean

added theorem nat.cast_add

added theorem nat.cast_add_one

added theorem nat.cast_bit0

added theorem nat.cast_bit1

added theorem nat.cast_eq_zero

added theorem nat.cast_id

added theorem nat.cast_inj

added theorem nat.cast_le

added theorem nat.cast_lt

added theorem nat.cast_mul

added theorem nat.cast_ne_zero

added theorem nat.cast_nonneg

added theorem nat.cast_one

added theorem nat.cast_pos

added theorem nat.cast_pred

added theorem nat.cast_sub

added theorem nat.cast_succ

added theorem nat.cast_zero

added theorem nat.mul_cast_comm

Modified data/num/basic.lean

deleted def int.of_znum

deleted def int.znum_coe

deleted def nat.of_num

deleted def nat.of_pos_num

deleted def num.nat_num_coe

modified def nzsnum.drec'

modified def snum.drec'

added def znum.cmp

Modified data/num/bitwise.lean

Modified data/num/lemmas.lean

deleted theorem num.add_to_nat

added theorem num.cast_add

added theorem num.cast_cmp'

added theorem num.cast_cmp

added theorem num.cast_inj

added theorem num.cast_le

added theorem num.cast_lt

added theorem num.cast_mul

added theorem num.cast_one

added theorem num.cast_succ'

added theorem num.cast_succ

added theorem num.cast_zero

deleted theorem num.cmp_dec

added theorem num.cmp_eq

modified theorem num.lt_iff_cmp

deleted theorem num.mul_to_nat

deleted theorem num.one_to_nat

deleted theorem num.succ'_to_nat

deleted theorem num.succ_to_nat

deleted theorem num.zero_to_nat

deleted theorem pos_num.add_to_nat

added theorem pos_num.cast_add

added theorem pos_num.cast_add_comm

added theorem pos_num.cast_add_comm_lemma_1

added theorem pos_num.cast_add_comm_lemma_2

added theorem pos_num.cast_add_one_comm

added theorem pos_num.cast_cmp'

added theorem pos_num.cast_cmp

added theorem pos_num.cast_inj

added theorem pos_num.cast_le

added theorem pos_num.cast_lt

added theorem pos_num.cast_mul

added theorem pos_num.cast_one

added theorem pos_num.cast_pos

added theorem pos_num.cast_succ

deleted theorem pos_num.cmp_dec

deleted theorem pos_num.cmp_dec_theorem

added theorem pos_num.cmp_eq

modified theorem pos_num.lt_iff_cmp

deleted theorem pos_num.mul_to_nat

added theorem pos_num.one_le_cast

deleted theorem pos_num.one_to_nat

deleted theorem pos_num.succ_to_nat

modified theorem pos_num.to_nat_inj

deleted theorem pos_num.to_nat_pos

added theorem znum.cast_one

added theorem znum.cast_zero

Deleted data/num/norm_num.lean

deleted theorem norm_num.bit0_le_one

deleted theorem norm_num.bit0_le_zero

deleted theorem norm_num.bit1_le_bit0

deleted theorem norm_num.bit1_le_one

deleted theorem norm_num.bit1_le_zero

deleted theorem norm_num.one_le_bit0

deleted theorem norm_num.one_le_bit1

deleted theorem norm_num.one_le_one

deleted theorem norm_num.pow_bit0

deleted theorem norm_num.pow_bit0_helper

deleted theorem norm_num.pow_bit1

deleted theorem norm_num.pow_bit1_helper

deleted theorem norm_num.pow_eq_pow_nat

deleted theorem norm_num.pow_eq_pow_nat_helper

deleted theorem norm_num.pow_one

deleted theorem norm_num.pow_zero

deleted theorem norm_num.zero_le_bit0

deleted theorem norm_num.zero_le_bit1

deleted theorem norm_num.zero_le_one

deleted theorem norm_num.zero_le_zero

deleted def num.add1

deleted def num.add_n

deleted theorem num.bit0_le_bit0

deleted theorem num.denote_add1

deleted theorem num.denote_le_denote_of_num_le

deleted theorem num.denote_le_denote_of_pos_num_le

deleted theorem num.denote_le_denote_of_znum_le

deleted def num.num_le

deleted theorem num.one_le_denote

deleted def num.pos_le

deleted theorem num.zero_le_denote

deleted def num.znum_le

deleted inductive tactic.interactive.denotation

deleted def tactic.interactive.znum.to_neg

deleted def tactic.interactive.znum.to_pos

Modified data/option.lean

added theorem option.bind_eq_some

added theorem option.bind_none

modified theorem option.bind_some

modified def option.filter

modified def option.guard

modified theorem option.guard_eq_some

modified def option.iget

added theorem option.is_some_iff_exists

added theorem option.map_eq_some

added theorem option.map_none

added theorem option.map_some

modified theorem option.mem_def

added theorem option.none_ne_some

modified theorem option.some_inj

Modified data/rat.lean

deleted def linear_order_cases_on

deleted theorem linear_order_cases_on_eq

deleted theorem linear_order_cases_on_gt

deleted theorem linear_order_cases_on_lt

deleted theorem mul_nonneg_iff_right_nonneg_of_pos

added theorem rat.cast_add

added theorem rat.cast_add_of_ne_zero

added theorem rat.cast_bit0

added theorem rat.cast_bit1

added theorem rat.cast_coe_int

added theorem rat.cast_coe_nat

added theorem rat.cast_eq_zero

added theorem rat.cast_id

added theorem rat.cast_inj

added theorem rat.cast_le

added theorem rat.cast_lt

added theorem rat.cast_lt_zero

added theorem rat.cast_mk

added theorem rat.cast_mk_of_ne_zero

added theorem rat.cast_mul

added theorem rat.cast_mul_of_ne_zero

added theorem rat.cast_ne_zero

added theorem rat.cast_neg

added theorem rat.cast_nonneg

added theorem rat.cast_nonpos

added theorem rat.cast_of_int

added theorem rat.cast_one

added theorem rat.cast_pos

added theorem rat.cast_sub

added theorem rat.cast_sub_of_ne_zero

added theorem rat.cast_zero

deleted theorem rat.coe_int_add

modified theorem rat.coe_int_eq_mk

added theorem rat.coe_int_eq_of_int

deleted theorem rat.coe_int_inj

deleted theorem rat.coe_int_le

deleted theorem rat.coe_int_lt

deleted theorem rat.coe_int_mul

deleted theorem rat.coe_int_neg

deleted theorem rat.coe_int_one

deleted theorem rat.coe_int_sub

deleted theorem rat.coe_nat_rat_eq_mk

added theorem rat.denom_dvd

added theorem rat.mk_eq_div

added theorem rat.mul_cast_comm

added theorem rat.num_dvd

added theorem rat.of_int_eq_mk

Modified data/set/enumerate.lean

Deleted meta/expr.lean