Commit 2020-05-18 13:38 8b422458

View on Github →

refactor(algebra): merge init_.algebra into algebra (#2707) This is a big refactor PR. It depends on #2697, which brings in the algebra hierarchy without any change to the file structure. This PR merges init_.algebra.group into algebra.group and so on for the rest of the algebraic hierarchy.

Estimated changes

modified theorem add_div'
added theorem add_div_eq_mul_add_div
modified theorem div_add'
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
modified theorem div_sub'
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
modified theorem inv_one
added theorem inv_zero
deleted theorem is_ring_hom.injective
deleted theorem is_ring_hom.map_div
deleted theorem is_ring_hom.map_eq_zero
deleted theorem is_ring_hom.map_inv
deleted theorem is_ring_hom.map_ne_zero
modified theorem mul_div_assoc'
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
modified theorem neg_div'
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
modified theorem sub_div'
added theorem zero_div
modified theorem add_add_neg_cancel'_right
modified theorem add_add_sub_cancel
added theorem add_eq_of_eq_sub'
added theorem add_eq_of_eq_sub
added theorem add_sub
added theorem add_sub_assoc
modified theorem add_sub_cancel'
modified theorem add_sub_cancel'_right
added theorem add_sub_cancel
added theorem add_sub_comm
modified theorem add_sub_sub_cancel
modified theorem bit0_zero
modified theorem bit1_zero
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
modified theorem inv_involutive
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
modified theorem inv_unique
modified theorem left_inverse_add_left_sub
modified theorem left_inverse_sub_add_left
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
modified theorem mul_left_inj
modified theorem mul_left_injective
added theorem mul_left_inv
modified theorem mul_mul_mul_comm
added theorem mul_one
added theorem mul_right_cancel
added theorem mul_right_cancel_iff
added theorem mul_right_comm
modified theorem mul_right_inj
modified theorem mul_right_injective
added theorem mul_right_inv
modified theorem neg_add'
added theorem neg_add_eq_sub
added theorem neg_neg_sub_neg
added theorem neg_sub
modified theorem neg_sub_neg
added theorem one_inv
added theorem one_mul
added theorem sub_add
modified theorem sub_add_add_cancel
added theorem sub_add_cancel
added theorem sub_add_eq_add_sub
added theorem sub_add_eq_sub_sub
modified theorem sub_add_sub_cancel'
modified theorem sub_add_sub_cancel
added theorem sub_eq_add_neg
modified theorem sub_eq_neg_add
added theorem sub_eq_of_eq_add'
added theorem sub_eq_of_eq_add
added theorem sub_eq_sub_add_sub
modified theorem sub_eq_sub_iff_add_eq_add
modified theorem sub_eq_sub_iff_sub_eq_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
modified theorem sub_right_comm
added theorem sub_self
added theorem sub_sub
modified theorem sub_sub_cancel
added theorem sub_sub_self
modified theorem sub_sub_sub_cancel_left
modified theorem sub_sub_sub_cancel_right
added theorem sub_zero
added theorem zero_sub
deleted theorem is_unit.coe_lift_right
deleted theorem is_unit.map
deleted theorem is_unit.mul_left_inj
deleted theorem is_unit.mul_right_inj
deleted def is_unit
deleted theorem is_unit_iff_exists_inv'
deleted theorem is_unit_iff_exists_inv
deleted theorem is_unit_nat
deleted theorem is_unit_of_mul_eq_one
deleted theorem is_unit_one
deleted theorem is_unit_unit
deleted theorem units.is_unit_mul_units
modified def divp
modified theorem divp_assoc
modified theorem divp_divp_eq_divp_mul
modified theorem divp_eq_iff_mul_eq
modified theorem divp_eq_one_iff_eq
modified theorem divp_inv
modified theorem divp_left_inj
modified theorem divp_mul_cancel
modified theorem divp_one
modified theorem divp_self
added theorem is_unit.mul_left_inj
added theorem is_unit.mul_right_inj
added def is_unit
added theorem is_unit_iff_exists_inv
added theorem is_unit_of_mul_eq_one
added theorem is_unit_one
added theorem is_unit_unit
modified theorem mul_divp_cancel
deleted theorem nat.add_units_eq_zero
deleted theorem nat.units_eq_one
modified theorem one_divp
deleted theorem units.coe_val_hom
deleted def units.val_hom
modified theorem div_eq_div_iff
modified theorem div_eq_iff
modified theorem eq_div_iff
added theorem abs_div
modified theorem abs_inv
added theorem abs_one_div
added theorem add_halves
added theorem add_midpoint
added theorem add_self_div_two
modified theorem div_le_div_of_le_left
modified theorem div_le_div_of_le_of_nonneg
added theorem div_le_of_le_mul
added theorem div_neg_of_neg_of_pos
added theorem div_neg_of_pos_of_neg
modified theorem div_nonneg'
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
modified theorem inv_le_inv_of_le
modified theorem inv_le_one
modified theorem inv_lt_one
modified theorem inv_nonneg
modified theorem inv_nonpos
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
modified theorem mul_self_inj_of_nonneg
deleted theorem nat.inv_pos_of_nat
deleted theorem nat.one_div_le_one_div
deleted theorem nat.one_div_lt_one_div
deleted theorem nat.one_div_pos_of_nat
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
modified theorem one_le_inv
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 def abs
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_le_of_le_of_neg_le
added theorem abs_lt_of_lt_of_neg_lt
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_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_zero
added theorem add_le_add
added theorem add_le_add_left
added theorem add_le_add_right
added theorem add_le_add_three
modified theorem add_le_iff_nonpos_left
modified theorem add_le_iff_nonpos_right
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
modified theorem add_lt_iff_neg_left
modified theorem add_lt_iff_neg_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 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 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 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_add_le_of_le_add
added theorem neg_add_lt_of_lt_add
added theorem neg_le_abs_self
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 abs_mul
added theorem abs_mul_abs_self
added theorem abs_mul_self
added theorem abs_sub_square
modified theorem abs_two
modified theorem bit0_le_bit0
modified theorem bit0_lt_bit0
modified theorem bit1_le_bit1
modified theorem bit1_lt_bit1
modified theorem bit1_pos'
modified theorem bit1_pos
modified theorem decidable.mul_le_mul_left
modified theorem decidable.mul_le_mul_right
added theorem four_pos
modified theorem le_mul_iff_one_le_left
modified theorem le_mul_iff_one_le_right
modified theorem le_mul_of_one_le_left'
modified theorem le_mul_of_one_le_right'
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
modified theorem lt_mul_iff_one_lt_left
modified theorem lt_mul_iff_one_lt_right
modified theorem lt_mul_of_one_lt_right'
added theorem lt_of_mul_lt_mul_left
added theorem lt_of_mul_lt_mul_right
modified theorem mul_le_iff_le_one_left
modified theorem mul_le_iff_le_one_right
added theorem mul_le_mul
modified theorem mul_le_mul_left
modified theorem mul_le_mul_right
modified theorem mul_le_of_le_one_left
modified theorem mul_le_of_le_one_right
modified theorem mul_le_one
modified theorem mul_lt_iff_lt_one_left
modified theorem mul_lt_iff_lt_one_right
modified theorem mul_lt_mul''
added theorem mul_lt_mul'
added theorem mul_lt_mul
modified theorem mul_lt_mul_left
added theorem mul_lt_mul_of_neg_left
added theorem mul_lt_mul_of_pos_left
modified theorem mul_lt_mul_right
added theorem mul_neg_of_neg_of_pos
added theorem mul_neg_of_pos_of_neg
modified theorem mul_nonneg'
added theorem mul_nonneg
modified theorem mul_pos'
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
modified theorem neg_of_mul_pos_left
modified theorem neg_of_mul_pos_right
modified theorem nonpos_of_mul_nonneg_left
modified theorem nonpos_of_mul_nonneg_right
modified theorem one_le_bit1
modified theorem one_lt_bit1
modified theorem one_lt_mul
modified theorem one_lt_mul_of_le_of_lt
modified theorem one_lt_mul_of_lt_of_le
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
deleted theorem with_top.add_one_le_of_lt
deleted theorem with_top.coe_nat
deleted theorem with_top.nat_induction
deleted theorem with_top.nat_ne_top
deleted theorem with_top.top_ne_nat
added theorem zero_gt_neg_one
modified theorem zero_le_bit0
modified theorem zero_le_mul_left
modified theorem zero_le_mul_right
added theorem zero_le_one
modified theorem zero_lt_bit0
modified theorem zero_lt_mul_left
modified theorem zero_lt_mul_right
added theorem zero_lt_one
added def add_mul
added theorem add_mul_self_eq
added theorem distrib_three_right
modified theorem domain.mul_left_inj
modified theorem domain.mul_right_inj
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
modified theorem dvd_add_left
modified theorem dvd_add_right
modified theorem dvd_add_self_left
modified theorem dvd_add_self_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
modified theorem dvd_neg
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
deleted theorem is_ring_hom.comp
deleted theorem is_ring_hom.map_neg
deleted theorem is_ring_hom.map_sub
deleted theorem is_ring_hom.map_zero
deleted theorem is_ring_hom.of_semiring
deleted theorem is_semiring_hom.comp
added theorem left_distrib
added def mul_add
added theorem mul_dvd_mul
modified theorem mul_dvd_mul_iff_left
modified theorem mul_dvd_mul_iff_right
added theorem mul_dvd_mul_left
added theorem mul_dvd_mul_right
modified theorem mul_eq_zero
modified theorem mul_ne_zero'
added theorem mul_ne_zero
modified theorem mul_ne_zero_comm'
modified theorem mul_neg_one
added theorem mul_self_eq_one_iff
modified theorem mul_self_eq_zero
modified theorem mul_self_sub_mul_self
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
modified theorem neg_dvd
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
modified theorem neg_one_mul
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
deleted theorem ring_hom.coe_of
modified theorem ring_hom.id_apply
deleted def ring_hom.of
added def sub_mul
added theorem two_mul
modified theorem units.inv_eq_self_iff
modified theorem zero_dvd_iff
modified theorem zero_eq_mul
modified theorem zero_eq_mul_self
added theorem zero_mul
added theorem zero_ne_one
deleted theorem add_div_eq_mul_add_div
deleted theorem div_add_div
deleted theorem div_add_div_same
deleted theorem div_div_div_div_eq
deleted theorem div_div_eq_div_mul
deleted theorem div_div_eq_mul_div
deleted theorem div_eq_mul_one_div
deleted theorem div_eq_one_iff_eq
deleted theorem div_helper
deleted theorem div_mul_cancel
deleted theorem div_mul_div
deleted theorem div_mul_eq_mul_div
deleted theorem div_mul_eq_mul_div_comm
deleted theorem div_mul_left
deleted theorem div_mul_right
deleted theorem div_neg_eq_neg_div
deleted theorem div_one
deleted theorem div_self
deleted theorem div_sub_div
deleted theorem div_sub_div_same
deleted theorem div_zero
deleted theorem division_def
deleted theorem division_ring.mul_ne_zero
deleted theorem eq_div_iff_mul_eq
deleted theorem eq_div_of_mul_eq
deleted theorem eq_of_div_eq_one
deleted theorem eq_of_one_div_eq_one_div
deleted theorem eq_one_div_of_mul_eq_one
deleted theorem inv_eq_one_div
deleted theorem inv_inv'
deleted theorem inv_mul_cancel
deleted theorem inv_ne_zero
deleted theorem inv_zero
deleted theorem mul_div_assoc
deleted theorem mul_div_cancel'
deleted theorem mul_div_cancel
deleted theorem mul_div_cancel_left
deleted theorem mul_div_mul_left
deleted theorem mul_div_mul_right
deleted theorem mul_eq_mul_of_div_eq_div
deleted theorem mul_eq_of_eq_div
deleted theorem mul_inv'
deleted theorem mul_inv_cancel
deleted theorem mul_mul_div
deleted theorem mul_ne_zero_comm
deleted theorem mul_one_div_cancel
deleted theorem neg_div
deleted theorem neg_div_neg_eq
deleted theorem one_div_add_one_div
deleted theorem one_div_div
deleted theorem one_div_eq_inv
deleted theorem one_div_mul_cancel
deleted theorem one_div_mul_one_div
deleted theorem one_div_ne_zero
deleted theorem one_div_one
deleted theorem one_div_one_div
deleted theorem one_inv_eq
deleted theorem zero_div
deleted theorem abs_abs
deleted theorem abs_add_le_abs_add_abs
deleted theorem abs_add_three
deleted theorem abs_by_cases
deleted theorem abs_div
deleted theorem abs_le_of_le_of_neg_le
deleted theorem abs_lt_of_lt_of_neg_lt
deleted theorem abs_mul
deleted theorem abs_mul_abs_self
deleted theorem abs_mul_self
deleted theorem abs_neg
deleted theorem abs_nonneg
deleted theorem abs_of_neg
deleted theorem abs_of_nonneg
deleted theorem abs_of_nonpos
deleted theorem abs_of_pos
deleted theorem abs_one_div
deleted theorem abs_pos_of_ne_zero
deleted theorem abs_pos_of_neg
deleted theorem abs_pos_of_pos
deleted theorem abs_sub
deleted theorem abs_sub_abs_le_abs_sub
deleted theorem abs_sub_le
deleted theorem abs_sub_square
deleted theorem abs_zero
deleted theorem dist_bdd_within_interval
deleted theorem eq_of_abs_sub_eq_zero
deleted theorem eq_zero_of_abs_eq_zero
deleted theorem eq_zero_of_neg_eq
deleted theorem le_abs_self
deleted theorem max_add_add_left
deleted theorem max_add_add_right
deleted theorem max_eq_neg_min_neg_neg
deleted theorem max_neg_neg
deleted theorem min_add_add_left
deleted theorem min_add_add_right
deleted theorem min_eq_neg_max_neg_neg
deleted theorem min_neg_neg
deleted theorem ne_zero_of_abs_ne_zero
deleted theorem neg_le_abs_self
deleted theorem sub_le_of_abs_sub_le_left
deleted theorem sub_lt_of_abs_sub_lt_left
deleted theorem add_eq_of_eq_sub'
deleted theorem add_eq_of_eq_sub
deleted def add_neg_self
deleted theorem add_sub
deleted theorem add_sub_add_left_eq_sub
deleted theorem add_sub_add_right_eq_sub
deleted theorem add_sub_assoc
deleted theorem add_sub_cancel
deleted theorem add_sub_comm
deleted theorem eq_add_of_sub_eq'
deleted theorem eq_add_of_sub_eq
deleted theorem eq_inv_mul_of_mul_eq
deleted theorem eq_inv_of_eq_inv
deleted theorem eq_inv_of_mul_eq_one
deleted theorem eq_mul_inv_of_mul_eq
deleted theorem eq_mul_of_inv_mul_eq
deleted theorem eq_mul_of_mul_inv_eq
deleted theorem eq_of_sub_eq_zero
deleted theorem eq_sub_of_add_eq'
deleted theorem eq_sub_of_add_eq
deleted theorem group.mul_left_cancel
deleted theorem group.mul_right_cancel
deleted theorem inv_eq_of_mul_eq_one
deleted theorem inv_inj
deleted theorem inv_inv
deleted theorem inv_mul_cancel_left
deleted theorem inv_mul_cancel_right
deleted theorem inv_mul_eq_of_eq_mul
deleted def inv_mul_self
deleted theorem mul_assoc
deleted theorem mul_comm
deleted theorem mul_eq_of_eq_inv_mul
deleted theorem mul_eq_of_eq_mul_inv
deleted theorem mul_inv
deleted theorem mul_inv_cancel_left
deleted theorem mul_inv_cancel_right
deleted theorem mul_inv_eq_of_eq_mul
deleted theorem mul_inv_rev
deleted def mul_inv_self
deleted theorem mul_left_cancel
deleted theorem mul_left_cancel_iff
deleted theorem mul_left_comm
deleted theorem mul_left_inv
deleted theorem mul_one
deleted theorem mul_right_cancel
deleted theorem mul_right_cancel_iff
deleted theorem mul_right_comm
deleted theorem mul_right_inv
deleted theorem neg_add_eq_sub
deleted def neg_add_self
deleted theorem neg_neg_sub_neg
deleted theorem neg_sub
deleted theorem one_inv
deleted theorem one_mul
deleted theorem sub_add
deleted theorem sub_add_cancel
deleted theorem sub_add_eq_add_sub
deleted theorem sub_add_eq_sub_sub
deleted theorem sub_add_eq_sub_sub_swap
deleted theorem sub_eq_add_neg
deleted theorem sub_eq_of_eq_add'
deleted theorem sub_eq_of_eq_add
deleted theorem sub_eq_sub_add_sub
deleted theorem sub_eq_zero_iff_eq
deleted theorem sub_eq_zero_of_eq
deleted theorem sub_ne_zero_of_ne
deleted theorem sub_neg_eq_add
deleted theorem sub_self
deleted theorem sub_sub
deleted theorem sub_sub_self
deleted theorem sub_zero
deleted theorem zero_sub
deleted theorem add_halves
deleted theorem add_midpoint
deleted theorem add_self_div_two
deleted theorem div_le_div_of_le_of_neg
deleted theorem div_le_div_of_le_of_pos
deleted theorem div_le_of_le_mul
deleted theorem div_le_of_mul_le_of_neg
deleted theorem div_lt_div_of_lt_of_neg
deleted theorem div_lt_div_of_lt_of_pos
deleted theorem div_lt_of_mul_gt_of_neg
deleted theorem div_lt_of_mul_lt_of_pos
deleted theorem div_neg_of_neg_of_pos
deleted theorem div_neg_of_pos_of_neg
deleted theorem div_pos_of_neg_of_neg
deleted theorem div_pos_of_pos_of_pos
deleted theorem div_two_lt_of_pos
deleted theorem div_two_sub_self
deleted theorem ge_of_forall_ge_sub
deleted theorem le_div_of_mul_le
deleted theorem le_mul_of_div_le
deleted theorem le_mul_of_ge_one_left
deleted theorem le_mul_of_ge_one_right
deleted theorem le_of_one_div_le_one_div
deleted theorem le_of_one_le_div
deleted theorem lt_div_of_mul_lt
deleted theorem lt_mul_of_gt_one_right
deleted theorem lt_of_one_div_lt_one_div
deleted theorem lt_of_one_lt_div
deleted theorem mul_le_mul_of_mul_div_le
deleted theorem mul_le_of_div_le_of_neg
deleted theorem mul_le_of_le_div
deleted theorem mul_lt_of_gt_div_of_neg
deleted theorem mul_lt_of_lt_div
deleted theorem mul_sub_mul_div_mul_neg
deleted theorem neg_of_one_div_neg
deleted theorem one_div_le_neg_one
deleted theorem one_div_le_one_div_of_le
deleted theorem one_div_lt_neg_one
deleted theorem one_div_lt_one_div_of_lt
deleted theorem one_div_neg_of_neg
deleted theorem one_div_pos_of_pos
deleted theorem one_le_div_of_le
deleted theorem one_le_one_div
deleted theorem one_lt_div_of_lt
deleted theorem one_lt_one_div
deleted theorem pos_of_one_div_pos
deleted theorem sub_self_div_two
deleted theorem add_le_add
deleted theorem add_le_add_left
deleted theorem add_le_add_right
deleted theorem add_le_add_three
deleted theorem add_le_of_le_neg_add
deleted theorem add_le_of_le_of_nonpos
deleted theorem add_le_of_le_sub_left
deleted theorem add_le_of_le_sub_right
deleted theorem add_le_of_nonpos_of_le
deleted theorem add_lt_add
deleted theorem add_lt_add_left
deleted theorem add_lt_add_of_le_of_lt
deleted theorem add_lt_add_of_lt_of_le
deleted theorem add_lt_add_right
deleted theorem add_lt_of_le_of_neg
deleted theorem add_lt_of_lt_neg_add
deleted theorem add_lt_of_lt_of_neg
deleted theorem add_lt_of_lt_of_nonpos
deleted theorem add_lt_of_lt_sub_left
deleted theorem add_lt_of_lt_sub_right
deleted theorem add_lt_of_neg_of_le
deleted theorem add_lt_of_neg_of_lt
deleted theorem add_lt_of_nonpos_of_lt
deleted theorem add_neg
deleted theorem add_neg_of_neg_of_nonpos
deleted theorem add_neg_of_nonpos_of_neg
deleted theorem add_nonneg
deleted theorem add_nonpos
deleted theorem add_pos
deleted theorem add_pos_of_nonneg_of_pos
deleted theorem add_pos_of_pos_of_nonneg
deleted theorem le_add_of_le_of_nonneg
deleted theorem le_add_of_neg_add_le
deleted theorem le_add_of_neg_add_le_left
deleted theorem le_add_of_neg_le_sub_left
deleted theorem le_add_of_nonneg_left
deleted theorem le_add_of_nonneg_of_le
deleted theorem le_add_of_nonneg_right
deleted theorem le_add_of_sub_left_le
deleted theorem le_add_of_sub_right_le
deleted theorem le_neg_add_of_add_le
deleted theorem le_neg_of_le_neg
deleted theorem le_of_add_le_add_left
deleted theorem le_of_add_le_add_right
deleted theorem le_of_neg_le_neg
deleted theorem le_of_sub_nonneg
deleted theorem le_of_sub_nonpos
deleted theorem le_sub_left_of_add_le
deleted theorem le_sub_right_of_add_le
deleted theorem lt_add_of_le_of_pos
deleted theorem lt_add_of_lt_of_nonneg
deleted theorem lt_add_of_lt_of_pos
deleted theorem lt_add_of_neg_add_lt
deleted theorem lt_add_of_neg_add_lt_left
deleted theorem lt_add_of_neg_lt_sub_left
deleted theorem lt_add_of_nonneg_of_lt
deleted theorem lt_add_of_pos_left
deleted theorem lt_add_of_pos_of_le
deleted theorem lt_add_of_pos_of_lt
deleted theorem lt_add_of_pos_right
deleted theorem lt_add_of_sub_left_lt
deleted theorem lt_add_of_sub_right_lt
deleted theorem lt_neg_add_of_add_lt
deleted theorem lt_neg_of_lt_neg
deleted theorem lt_of_add_lt_add_left
deleted theorem lt_of_add_lt_add_right
deleted theorem lt_of_neg_lt_neg
deleted theorem lt_of_sub_neg
deleted theorem lt_of_sub_pos
deleted theorem lt_sub_left_of_add_lt
deleted theorem lt_sub_right_of_add_lt
deleted theorem neg_add_le_left_of_le_add
deleted theorem neg_add_le_of_le_add
deleted theorem neg_add_lt_left_of_lt_add
deleted theorem neg_add_lt_of_lt_add
deleted theorem neg_le_neg
deleted theorem neg_le_of_neg_le
deleted theorem neg_le_sub_left_of_le_add
deleted theorem neg_lt_neg
deleted theorem neg_lt_of_neg_lt
deleted theorem neg_lt_sub_left_of_lt_add
deleted theorem neg_neg_of_pos
deleted theorem neg_nonneg_of_nonpos
deleted theorem neg_nonpos_of_nonneg
deleted theorem neg_of_neg_pos
deleted theorem neg_pos_of_neg
deleted theorem nonneg_of_neg_nonpos
deleted theorem nonpos_of_neg_nonneg
deleted theorem pos_of_neg_neg
deleted theorem sub_le_of_sub_le
deleted theorem sub_le_self
deleted theorem sub_le_sub
deleted theorem sub_le_sub_left
deleted theorem sub_le_sub_right
deleted theorem sub_left_le_of_le_add
deleted theorem sub_left_lt_of_lt_add
deleted theorem sub_lt_of_sub_lt
deleted theorem sub_lt_self
deleted theorem sub_lt_sub
deleted theorem sub_lt_sub_left
deleted theorem sub_lt_sub_of_le_of_lt
deleted theorem sub_lt_sub_of_lt_of_le
deleted theorem sub_lt_sub_right
deleted theorem sub_neg_of_lt
deleted theorem sub_nonneg_of_le
deleted theorem sub_nonpos_of_le
deleted theorem sub_pos_of_lt
deleted theorem sub_right_le_of_le_add
deleted theorem sub_right_lt_of_lt_add
deleted theorem four_pos
deleted theorem gt_of_mul_lt_mul_neg_left
deleted theorem le_of_mul_le_mul_left
deleted theorem le_of_mul_le_mul_right
deleted theorem le_of_mul_le_of_ge_one
deleted theorem lt_of_mul_lt_mul_left
deleted theorem lt_of_mul_lt_mul_right
deleted theorem mul_le_mul
deleted theorem mul_le_mul_of_nonneg_left
deleted theorem mul_le_mul_of_nonpos_left
deleted theorem mul_lt_mul'
deleted theorem mul_lt_mul
deleted theorem mul_lt_mul_of_neg_left
deleted theorem mul_lt_mul_of_neg_right
deleted theorem mul_lt_mul_of_pos_left
deleted theorem mul_lt_mul_of_pos_right
deleted theorem mul_neg_of_neg_of_pos
deleted theorem mul_neg_of_pos_of_neg
deleted theorem mul_nonneg
deleted theorem mul_pos
deleted theorem mul_pos_of_neg_of_neg
deleted theorem mul_self_le_mul_self
deleted theorem mul_self_le_mul_self_iff
deleted theorem mul_self_lt_mul_self
deleted theorem mul_self_lt_mul_self_iff
deleted theorem mul_self_nonneg
deleted theorem neg_of_mul_neg_left
deleted theorem neg_of_mul_neg_right
deleted theorem nonneg_of_mul_nonneg_left
deleted theorem nonpos_of_mul_nonpos_left
deleted theorem ordered_ring.mul_nonneg
deleted theorem pos_of_mul_pos_left
deleted theorem pos_of_mul_pos_right
deleted theorem two_ge_one
deleted theorem two_gt_one
deleted theorem two_ne_zero
deleted theorem two_pos
deleted theorem zero_gt_neg_one
deleted theorem zero_le_one
deleted theorem zero_lt_one
deleted def add_mul
deleted theorem add_mul_self_eq
deleted theorem distrib_three_right
deleted theorem dvd.elim
deleted theorem dvd.elim_left
deleted theorem dvd.intro
deleted theorem dvd.intro_left
deleted def dvd.trans
deleted theorem dvd_add
deleted theorem dvd_add_iff_left
deleted theorem dvd_add_iff_right
deleted theorem dvd_mul_left
deleted theorem dvd_mul_of_dvd_left
deleted theorem dvd_mul_of_dvd_right
deleted theorem dvd_mul_right
deleted theorem dvd_neg_iff_dvd
deleted theorem dvd_neg_of_dvd
deleted theorem dvd_of_dvd_neg
deleted theorem dvd_of_mul_left_dvd
deleted def dvd_of_mul_left_eq
deleted theorem dvd_of_mul_right_dvd
deleted def dvd_of_mul_right_eq
deleted theorem dvd_of_neg_dvd
deleted theorem dvd_refl
deleted theorem dvd_sub
deleted theorem dvd_trans
deleted theorem dvd_zero
deleted theorem eq_of_mul_eq_mul_left
deleted theorem eq_of_mul_eq_mul_right
deleted theorem eq_zero_of_zero_dvd
deleted theorem exists_eq_mul_left_of_dvd
deleted theorem left_distrib
deleted def mul_add
deleted theorem mul_dvd_mul
deleted theorem mul_dvd_mul_left
deleted theorem mul_dvd_mul_right
deleted theorem mul_ne_zero
deleted theorem mul_neg_eq_neg_mul_symm
deleted theorem mul_self_eq_mul_self_iff
deleted theorem mul_self_eq_one_iff
deleted theorem mul_self_sub_mul_self_eq
deleted theorem mul_self_sub_one_eq
deleted def mul_sub
deleted theorem mul_sub_left_distrib
deleted theorem mul_sub_right_distrib
deleted theorem mul_zero
deleted theorem neg_dvd_iff_dvd
deleted theorem neg_dvd_of_dvd
deleted theorem neg_eq_neg_one_mul
deleted theorem neg_mul_comm
deleted theorem neg_mul_eq_mul_neg
deleted theorem neg_mul_eq_neg_mul
deleted theorem neg_mul_eq_neg_mul_symm
deleted theorem neg_mul_neg
deleted theorem one_add_one_eq_two
deleted theorem one_dvd
deleted theorem one_ne_zero
deleted theorem right_distrib
deleted theorem ring.mul_zero
deleted theorem ring.zero_mul
deleted def sub_mul
deleted theorem two_mul
deleted theorem zero_mul
deleted theorem zero_ne_one