Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-29 16:12 d3006bad

View on Github →

chore(init_/): remove this directory (#3227)

  • remove init_/algebra;
  • move init_/data/nat to data/nat/basic;
  • move init_/data/int to data/int/basic.

Estimated changes

added theorem int.abs_eq_nat_abs
added theorem int.nat_abs_abs
added theorem int.sign_mul_abs
added theorem nat.le_mul_self
added theorem nat.one_add
deleted def norm_num.add1
deleted theorem norm_num.add1_bit0
deleted theorem norm_num.add1_bit1
deleted theorem norm_num.add1_bit1_helper
deleted theorem norm_num.add1_one
deleted theorem norm_num.add1_zero
deleted theorem norm_num.add_comm_four
deleted theorem norm_num.add_comm_middle
deleted theorem norm_num.add_div_helper
deleted theorem norm_num.bin_add_zero
deleted theorem norm_num.bin_zero_add
deleted theorem norm_num.bit0_add_bit0
deleted theorem norm_num.bit0_add_bit1
deleted theorem norm_num.bit0_add_one
deleted theorem norm_num.bit1_add_bit0
deleted theorem norm_num.bit1_add_bit1
deleted theorem norm_num.bit1_add_one
deleted theorem norm_num.div_add_helper
deleted theorem norm_num.div_helper
deleted theorem norm_num.div_mul_helper
deleted theorem norm_num.mk_cong
deleted theorem norm_num.mul_bit0
deleted theorem norm_num.mul_bit0_helper
deleted theorem norm_num.mul_bit1
deleted theorem norm_num.mul_bit1_helper
deleted theorem norm_num.mul_div_helper
deleted theorem norm_num.mul_one
deleted theorem norm_num.mul_zero
deleted theorem norm_num.neg_neg_helper
deleted theorem norm_num.neg_zero_helper
deleted theorem norm_num.one_add_bit0
deleted theorem norm_num.one_add_bit1
deleted theorem norm_num.one_add_one
deleted theorem norm_num.pos_bit0_helper
deleted theorem norm_num.pos_bit1_helper
deleted theorem norm_num.subst_into_div
deleted theorem norm_num.subst_into_prod
deleted theorem norm_num.subst_into_subtr
deleted theorem norm_num.subst_into_sum
deleted theorem norm_num.zero_mul
deleted theorem int.abs_eq_nat_abs
deleted theorem int.nat_abs_abs
deleted theorem int.sign_mul_abs
deleted theorem nat.le_mul_self
deleted theorem nat.mul_self_le_mul_self
deleted theorem nat.mul_self_lt_mul_self
deleted theorem nat.one_add