Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-17 17:58 f23c361e

View on Github →

chore(*): bump to lean-3.13.1 (#2697)

Move algebra to mathlib

The algebraic hierarchy has moved from the core library to init_. In later PRs this can be integrated into the existing directory structure of mathlib.

Estimated changes

added theorem add_div_eq_mul_add_div
added theorem div_add_div
added theorem div_add_div_same
added theorem div_div_div_div_eq
added theorem div_div_eq_div_mul
added theorem div_div_eq_mul_div
added theorem div_eq_mul_one_div
added theorem div_eq_one_iff_eq
added theorem div_helper
added theorem div_mul_cancel
added theorem div_mul_div
added theorem div_mul_eq_mul_div
added theorem div_mul_left
added theorem div_mul_right
added theorem div_neg_eq_neg_div
added theorem div_one
added theorem div_self
added theorem div_sub_div
added theorem div_sub_div_same
added theorem div_zero
added theorem division_def
added theorem eq_div_iff_mul_eq
added theorem eq_div_of_mul_eq
added theorem eq_of_div_eq_one
added theorem inv_eq_one_div
added theorem inv_inv'
added theorem inv_mul_cancel
added theorem inv_ne_zero
added theorem inv_zero
added theorem mul_div_assoc
added theorem mul_div_cancel'
added theorem mul_div_cancel
added theorem mul_div_cancel_left
added theorem mul_div_mul_left
added theorem mul_div_mul_right
added theorem mul_eq_of_eq_div
added theorem mul_inv'
added theorem mul_inv_cancel
added theorem mul_mul_div
added theorem mul_ne_zero_comm
added theorem mul_one_div_cancel
added theorem neg_div
added theorem neg_div_neg_eq
added theorem one_div_add_one_div
added theorem one_div_div
added theorem one_div_eq_inv
added theorem one_div_mul_cancel
added theorem one_div_mul_one_div
added theorem one_div_ne_zero
added theorem one_div_one
added theorem one_div_one_div
added theorem one_inv_eq
added theorem zero_div
added theorem abs_abs
added theorem abs_add_le_abs_add_abs
added theorem abs_add_three
added theorem abs_by_cases
added theorem abs_div
added theorem abs_le_of_le_of_neg_le
added theorem abs_lt_of_lt_of_neg_lt
added theorem abs_mul
added theorem abs_mul_abs_self
added theorem abs_mul_self
added theorem abs_neg
added theorem abs_nonneg
added theorem abs_of_neg
added theorem abs_of_nonneg
added theorem abs_of_nonpos
added theorem abs_of_pos
added theorem abs_one_div
added theorem abs_pos_of_ne_zero
added theorem abs_pos_of_neg
added theorem abs_pos_of_pos
added theorem abs_sub
added theorem abs_sub_abs_le_abs_sub
added theorem abs_sub_le
added theorem abs_sub_square
added theorem abs_zero
added theorem eq_of_abs_sub_eq_zero
added theorem eq_zero_of_abs_eq_zero
added theorem eq_zero_of_neg_eq
added theorem le_abs_self
added theorem max_add_add_left
added theorem max_add_add_right
added theorem max_eq_neg_min_neg_neg
added theorem max_neg_neg
added theorem min_add_add_left
added theorem min_add_add_right
added theorem min_eq_neg_max_neg_neg
added theorem min_neg_neg
added theorem ne_zero_of_abs_ne_zero
added theorem neg_le_abs_self
added theorem add_eq_of_eq_sub'
added theorem add_eq_of_eq_sub
added def add_neg_self
added theorem add_sub
added theorem add_sub_assoc
added theorem add_sub_cancel
added theorem add_sub_comm
added theorem eq_add_of_sub_eq'
added theorem eq_add_of_sub_eq
added theorem eq_inv_mul_of_mul_eq
added theorem eq_inv_of_eq_inv
added theorem eq_inv_of_mul_eq_one
added theorem eq_mul_inv_of_mul_eq
added theorem eq_mul_of_inv_mul_eq
added theorem eq_mul_of_mul_inv_eq
added theorem eq_of_sub_eq_zero
added theorem eq_sub_of_add_eq'
added theorem eq_sub_of_add_eq
added theorem group.mul_left_cancel
added theorem group.mul_right_cancel
added theorem inv_eq_of_mul_eq_one
added theorem inv_inj
added theorem inv_inv
added theorem inv_mul_cancel_left
added theorem inv_mul_cancel_right
added theorem inv_mul_eq_of_eq_mul
added def inv_mul_self
added theorem mul_assoc
added theorem mul_comm
added theorem mul_eq_of_eq_inv_mul
added theorem mul_eq_of_eq_mul_inv
added theorem mul_inv
added theorem mul_inv_cancel_left
added theorem mul_inv_cancel_right
added theorem mul_inv_eq_of_eq_mul
added theorem mul_inv_rev
added def mul_inv_self
added theorem mul_left_cancel
added theorem mul_left_cancel_iff
added theorem mul_left_comm
added theorem mul_left_inv
added theorem mul_one
added theorem mul_right_cancel
added theorem mul_right_cancel_iff
added theorem mul_right_comm
added theorem mul_right_inv
added theorem neg_add_eq_sub
added def neg_add_self
added theorem neg_neg_sub_neg
added theorem neg_sub
added theorem one_inv
added theorem one_mul
added theorem sub_add
added theorem sub_add_cancel
added theorem sub_add_eq_add_sub
added theorem sub_add_eq_sub_sub
added theorem sub_eq_add_neg
added theorem sub_eq_of_eq_add'
added theorem sub_eq_of_eq_add
added theorem sub_eq_sub_add_sub
added theorem sub_eq_zero_iff_eq
added theorem sub_eq_zero_of_eq
added theorem sub_ne_zero_of_ne
added theorem sub_neg_eq_add
added theorem sub_self
added theorem sub_sub
added theorem sub_sub_self
added theorem sub_zero
added theorem zero_sub
added def norm_num.add1
added theorem norm_num.add1_bit0
added theorem norm_num.add1_bit1
added theorem norm_num.add1_one
added theorem norm_num.add1_zero
added theorem norm_num.add_comm_four
added theorem norm_num.bin_add_zero
added theorem norm_num.bin_zero_add
added theorem norm_num.bit0_add_bit0
added theorem norm_num.bit0_add_bit1
added theorem norm_num.bit0_add_one
added theorem norm_num.bit1_add_bit0
added theorem norm_num.bit1_add_bit1
added theorem norm_num.bit1_add_one
added theorem norm_num.div_helper
added theorem norm_num.mk_cong
added theorem norm_num.mul_bit0
added theorem norm_num.mul_bit1
added theorem norm_num.mul_one
added theorem norm_num.mul_zero
added theorem norm_num.one_add_bit0
added theorem norm_num.one_add_bit1
added theorem norm_num.one_add_one
added theorem norm_num.zero_mul
added theorem add_halves
added theorem add_midpoint
added theorem add_self_div_two
added theorem div_le_of_le_mul
added theorem div_neg_of_neg_of_pos
added theorem div_neg_of_pos_of_neg
added theorem div_pos_of_neg_of_neg
added theorem div_pos_of_pos_of_pos
added theorem div_two_lt_of_pos
added theorem div_two_sub_self
added theorem ge_of_forall_ge_sub
added theorem le_div_of_mul_le
added theorem le_mul_of_div_le
added theorem le_mul_of_ge_one_left
added theorem le_mul_of_ge_one_right
added theorem le_of_one_le_div
added theorem lt_div_of_mul_lt
added theorem lt_mul_of_gt_one_right
added theorem lt_of_one_lt_div
added theorem mul_le_of_le_div
added theorem mul_lt_of_lt_div
added theorem neg_of_one_div_neg
added theorem one_div_le_neg_one
added theorem one_div_lt_neg_one
added theorem one_div_neg_of_neg
added theorem one_div_pos_of_pos
added theorem one_le_div_of_le
added theorem one_le_one_div
added theorem one_lt_div_of_lt
added theorem one_lt_one_div
added theorem pos_of_one_div_pos
added theorem sub_self_div_two
added theorem add_le_add
added theorem add_le_add_left
added theorem add_le_add_right
added theorem add_le_add_three
added theorem add_le_of_le_neg_add
added theorem add_le_of_le_of_nonpos
added theorem add_le_of_le_sub_left
added theorem add_le_of_le_sub_right
added theorem add_le_of_nonpos_of_le
added theorem add_lt_add
added theorem add_lt_add_left
added theorem add_lt_add_of_le_of_lt
added theorem add_lt_add_of_lt_of_le
added theorem add_lt_add_right
added theorem add_lt_of_le_of_neg
added theorem add_lt_of_lt_neg_add
added theorem add_lt_of_lt_of_neg
added theorem add_lt_of_lt_of_nonpos
added theorem add_lt_of_lt_sub_left
added theorem add_lt_of_lt_sub_right
added theorem add_lt_of_neg_of_le
added theorem add_lt_of_neg_of_lt
added theorem add_lt_of_nonpos_of_lt
added theorem add_neg
added theorem add_nonneg
added theorem add_nonpos
added theorem add_pos
added theorem le_add_of_le_of_nonneg
added theorem le_add_of_neg_add_le
added theorem le_add_of_nonneg_left
added theorem le_add_of_nonneg_of_le
added theorem le_add_of_nonneg_right
added theorem le_add_of_sub_left_le
added theorem le_add_of_sub_right_le
added theorem le_neg_add_of_add_le
added theorem le_neg_of_le_neg
added theorem le_of_add_le_add_left
added theorem le_of_add_le_add_right
added theorem le_of_neg_le_neg
added theorem le_of_sub_nonneg
added theorem le_of_sub_nonpos
added theorem le_sub_left_of_add_le
added theorem le_sub_right_of_add_le
added theorem lt_add_of_le_of_pos
added theorem lt_add_of_lt_of_nonneg
added theorem lt_add_of_lt_of_pos
added theorem lt_add_of_neg_add_lt
added theorem lt_add_of_nonneg_of_lt
added theorem lt_add_of_pos_left
added theorem lt_add_of_pos_of_le
added theorem lt_add_of_pos_of_lt
added theorem lt_add_of_pos_right
added theorem lt_add_of_sub_left_lt
added theorem lt_add_of_sub_right_lt
added theorem lt_neg_add_of_add_lt
added theorem lt_neg_of_lt_neg
added theorem lt_of_add_lt_add_left
added theorem lt_of_add_lt_add_right
added theorem lt_of_neg_lt_neg
added theorem lt_of_sub_neg
added theorem lt_of_sub_pos
added theorem lt_sub_left_of_add_lt
added theorem lt_sub_right_of_add_lt
added theorem neg_add_le_of_le_add
added theorem neg_add_lt_of_lt_add
added theorem neg_le_neg
added theorem neg_le_of_neg_le
added theorem neg_lt_neg
added theorem neg_lt_of_neg_lt
added theorem neg_neg_of_pos
added theorem neg_nonneg_of_nonpos
added theorem neg_nonpos_of_nonneg
added theorem neg_of_neg_pos
added theorem neg_pos_of_neg
added theorem nonneg_of_neg_nonpos
added theorem nonpos_of_neg_nonneg
added theorem pos_of_neg_neg
added theorem sub_le_of_sub_le
added theorem sub_le_self
added theorem sub_le_sub
added theorem sub_le_sub_left
added theorem sub_le_sub_right
added theorem sub_left_le_of_le_add
added theorem sub_left_lt_of_lt_add
added theorem sub_lt_of_sub_lt
added theorem sub_lt_self
added theorem sub_lt_sub
added theorem sub_lt_sub_left
added theorem sub_lt_sub_of_le_of_lt
added theorem sub_lt_sub_of_lt_of_le
added theorem sub_lt_sub_right
added theorem sub_neg_of_lt
added theorem sub_nonneg_of_le
added theorem sub_nonpos_of_le
added theorem sub_pos_of_lt
added theorem sub_right_le_of_le_add
added theorem sub_right_lt_of_lt_add
added theorem four_pos
added theorem le_of_mul_le_mul_left
added theorem le_of_mul_le_mul_right
added theorem le_of_mul_le_of_ge_one
added theorem lt_of_mul_lt_mul_left
added theorem lt_of_mul_lt_mul_right
added theorem mul_le_mul
added theorem mul_lt_mul'
added theorem mul_lt_mul
added theorem mul_lt_mul_of_neg_left
added theorem mul_lt_mul_of_pos_left
added theorem mul_neg_of_neg_of_pos
added theorem mul_neg_of_pos_of_neg
added theorem mul_nonneg
added theorem mul_pos
added theorem mul_pos_of_neg_of_neg
added theorem mul_self_le_mul_self
added theorem mul_self_lt_mul_self
added theorem mul_self_nonneg
added theorem neg_of_mul_neg_left
added theorem neg_of_mul_neg_right
added theorem pos_of_mul_pos_left
added theorem pos_of_mul_pos_right
added theorem two_ge_one
added theorem two_gt_one
added theorem two_ne_zero
added theorem two_pos
added theorem zero_gt_neg_one
added theorem zero_le_one
added theorem zero_lt_one
added def add_mul
added theorem add_mul_self_eq
added theorem distrib_three_right
added theorem dvd.elim
added theorem dvd.elim_left
added theorem dvd.intro
added theorem dvd.intro_left
added def dvd.trans
added theorem dvd_add
added theorem dvd_add_iff_left
added theorem dvd_add_iff_right
added theorem dvd_mul_left
added theorem dvd_mul_of_dvd_left
added theorem dvd_mul_of_dvd_right
added theorem dvd_mul_right
added theorem dvd_neg_iff_dvd
added theorem dvd_neg_of_dvd
added theorem dvd_of_dvd_neg
added theorem dvd_of_mul_left_dvd
added theorem dvd_of_mul_right_dvd
added theorem dvd_of_neg_dvd
added theorem dvd_refl
added theorem dvd_sub
added theorem dvd_trans
added theorem dvd_zero
added theorem eq_of_mul_eq_mul_left
added theorem eq_of_mul_eq_mul_right
added theorem eq_zero_of_zero_dvd
added theorem left_distrib
added def mul_add
added theorem mul_dvd_mul
added theorem mul_dvd_mul_left
added theorem mul_dvd_mul_right
added theorem mul_ne_zero
added theorem mul_self_eq_one_iff
added theorem mul_self_sub_one_eq
added def mul_sub
added theorem mul_sub_left_distrib
added theorem mul_sub_right_distrib
added theorem mul_zero
added theorem neg_dvd_iff_dvd
added theorem neg_dvd_of_dvd
added theorem neg_eq_neg_one_mul
added theorem neg_mul_comm
added theorem neg_mul_eq_mul_neg
added theorem neg_mul_eq_neg_mul
added theorem neg_mul_neg
added theorem one_add_one_eq_two
added theorem one_dvd
added theorem one_ne_zero
added theorem right_distrib
added theorem ring.mul_zero
added theorem ring.zero_mul
added def sub_mul
added theorem two_mul
added theorem zero_mul
added theorem zero_ne_one
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