Mathlib v3 is deprecated. Go to Mathlib v4

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 archive/100-theorems-list/42_inverse_triangle_sum.lean

Modified archive/sensitivity.lean

Modified scripts/nolints.txt

Modified src/algebra/char_zero.lean

Modified src/algebra/continued_fractions/basic.lean

Modified src/algebra/continued_fractions/convergents_equiv.lean

Modified src/algebra/field.lean

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_div_mul_one_div

added theorem div_mul_eq_mul_div

added theorem div_mul_eq_mul_div_comm

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 division_ring.mul_ne_zero

added theorem division_ring.one_div_mul_one_div

added theorem eq_div_iff_mul_eq

added theorem eq_div_of_mul_eq

added theorem eq_of_div_eq_one

added theorem eq_of_mul_eq_mul_of_nonzero_left

added theorem eq_of_mul_eq_mul_of_nonzero_right

added theorem eq_of_one_div_eq_one_div

added theorem eq_one_div_of_mul_eq_one

added theorem eq_one_div_of_mul_eq_one_left

added theorem eq_zero_of_one_div_eq_zero

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_mul_of_div_eq_div

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 ne_zero_of_one_div_ne_zero

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_add_mul_one_div_eq_one_div_add_one_div

added theorem one_div_mul_cancel

added theorem one_div_mul_one_div

added theorem one_div_mul_sub_mul_one_div_eq_one_div_add_one_div

added theorem one_div_ne_zero

added theorem one_div_neg_eq_neg_one_div

added theorem one_div_neg_one_eq_neg_one

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 src/algebra/floor.lean

Modified src/algebra/free.lean

Modified src/algebra/gcd_domain.lean

Modified src/algebra/group/basic.lean

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_add_left_eq_sub

added theorem add_sub_add_right_eq_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 def eq_of_add_eq_add_left

added def eq_of_add_eq_add_right

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_add_right_neg_add

modified theorem left_inverse_neg_add_add_right

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

added theorem sub_add_eq_sub_sub_swap

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

Modified src/algebra/group/conj.lean

Modified src/algebra/group/default.lean

Modified src/algebra/group/hom.lean

deleted theorem add_monoid_hom.coe_mul_left

deleted def add_monoid_hom.mul_left

deleted def add_monoid_hom.mul_right

deleted theorem add_monoid_hom.mul_right_apply

Deleted src/algebra/group/is_unit.lean

deleted theorem is_unit.coe_lift_right

deleted theorem is_unit.lift_right_inv_mul

deleted theorem is_unit.map

deleted theorem is_unit.mul_left_inj

deleted theorem is_unit.mul_lift_right_inv

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_of_mul_is_unit_left

deleted theorem is_unit_of_mul_is_unit_right

deleted theorem is_unit_one

deleted theorem is_unit_unit

deleted theorem units.is_unit_mul_units

Modified src/algebra/group/to_additive.lean

Modified src/algebra/group/units.lean

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_iff_exists_inv

added theorem is_unit_of_mul_eq_one

added theorem is_unit_of_mul_is_unit_left

added theorem is_unit_of_mul_is_unit_right

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

added theorem units.is_unit_mul_units

deleted def units.val_hom

Modified src/algebra/group/units_hom.lean

added theorem is_unit.coe_lift_right

added theorem is_unit.lift_right_inv_mul

added theorem is_unit.map

added theorem is_unit.mul_lift_right_inv

Modified src/algebra/group/with_one.lean

Modified src/algebra/group_power.lean

Modified src/algebra/group_ring_action.lean

Modified src/algebra/group_with_zero.lean

modified theorem div_eq_div_iff

modified theorem div_eq_iff

modified theorem eq_div_iff

Modified src/algebra/lie_algebra.lean

Modified src/algebra/opposites.lean

Modified src/algebra/ordered_field.lean

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

added theorem div_le_div_of_le_of_neg

modified theorem div_le_div_of_le_of_nonneg

added theorem div_le_div_of_le_of_pos

added theorem div_le_div_of_mul_sub_mul_div_nonpos

added theorem div_le_of_le_mul

added theorem div_le_of_mul_le_of_neg

added theorem div_lt_div_of_lt_of_neg

added theorem div_lt_div_of_lt_of_pos

added theorem div_lt_div_of_mul_sub_mul_div_neg

added theorem div_lt_div_of_pos_of_lt_of_pos

added theorem div_lt_of_mul_gt_of_neg

added theorem div_lt_of_mul_lt_of_pos

added theorem div_mul_le_div_mul_of_div_le_div_pos'

added theorem div_mul_le_div_mul_of_div_le_div_pos

added theorem div_neg_of_neg_of_pos

added theorem div_neg_of_pos_of_neg

modified theorem div_nonneg'

added theorem div_nonneg_of_nonneg_of_pos

added theorem div_nonneg_of_nonpos_of_neg

added theorem div_nonpos_of_nonneg_of_neg

added theorem div_nonpos_of_nonpos_of_pos

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 exists_add_lt_and_pos_of_lt

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_div_le_one_div

added theorem le_of_one_div_le_one_div_of_neg

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_div_lt_one_div

added theorem lt_of_one_div_lt_one_div_of_neg

added theorem lt_of_one_lt_div

added theorem mul_le_mul_of_mul_div_le

added theorem mul_le_of_div_le_of_neg

added theorem mul_le_of_le_div

added theorem mul_lt_of_gt_div_of_neg

added theorem mul_lt_of_lt_div

modified theorem mul_self_inj_of_nonneg

added theorem mul_sub_mul_div_mul_neg

added theorem mul_sub_mul_div_mul_nonpos

added theorem mul_zero_lt_mul_inv_of_neg

added theorem mul_zero_lt_mul_inv_of_pos

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_le_of_one_div_le_of_neg

added theorem one_div_le_of_one_div_le_of_pos

added theorem one_div_le_one_div_of_le

added theorem one_div_le_one_div_of_le_of_neg

added theorem one_div_lt_neg_one

added theorem one_div_lt_one_div_of_lt

added theorem one_div_lt_one_div_of_lt_of_neg

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

Modified src/algebra/ordered_group.lean

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_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg

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_neg_of_neg_of_nonpos

added theorem add_neg_of_nonpos_of_neg

added theorem add_nonneg

added theorem add_nonpos

added theorem add_pos

added theorem add_pos_of_nonneg_of_pos

added theorem add_pos_of_pos_of_nonneg

added theorem decidable_linear_ordered_add_comm_group.add_lt_add_left

modified theorem decidable_linear_ordered_add_comm_group.eq_of_abs_sub_nonpos

added theorem dist_bdd_within_interval

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_neg_add_le_left

added theorem le_add_of_neg_add_le_right

added theorem le_add_of_neg_le_sub_left

added theorem le_add_of_neg_le_sub_right

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_neg_add_lt_left

added theorem lt_add_of_neg_add_lt_right

added theorem lt_add_of_neg_lt_sub_left

added theorem lt_add_of_neg_lt_sub_right

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_left_of_le_add

added theorem neg_add_le_of_le_add

added theorem neg_add_le_right_of_le_add

added theorem neg_add_lt_left_of_lt_add

added theorem neg_add_lt_of_lt_add

added theorem neg_add_lt_right_of_lt_add

added theorem neg_le_abs_self

added theorem neg_le_neg

added theorem neg_le_of_neg_le

added theorem neg_le_sub_left_of_le_add

added theorem neg_le_sub_right_of_le_add

added theorem neg_lt_neg

added theorem neg_lt_of_neg_lt

added theorem neg_lt_sub_left_of_lt_add

added theorem neg_lt_sub_right_of_lt_add

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 ordered_add_comm_group.add_lt_add_left

added theorem ordered_add_comm_group.le_of_add_le_add_left

added theorem ordered_add_comm_group.lt_of_add_lt_add_left

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

Modified src/algebra/ordered_ring.lean

added theorem abs_abs_sub_abs_le_abs_sub

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 canonically_ordered_semiring.mul_pos

modified theorem decidable.mul_le_mul_left

modified theorem decidable.mul_le_mul_right

added theorem eq_zero_of_mul_self_add_mul_self_eq_zero

added theorem four_pos

added theorem gt_of_mul_lt_mul_neg_left

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

added theorem linear_ordered_ring.eq_zero_or_eq_zero_of_mul_eq_zero

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

added theorem mul_le_mul_of_nonneg_left

added theorem mul_le_mul_of_nonneg_right

added theorem mul_le_mul_of_nonpos_left

added theorem mul_le_mul_of_nonpos_right

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_neg_right

added theorem mul_lt_mul_of_pos_left

added theorem mul_lt_mul_of_pos_right

modified theorem mul_lt_mul_right

modified theorem mul_lt_one_of_nonneg_of_lt_one_left

modified theorem mul_lt_one_of_nonneg_of_lt_one_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_nonneg_iff_right_nonneg_of_pos

added theorem mul_nonneg_of_nonpos_of_nonpos

added theorem mul_nonpos_of_nonneg_of_nonpos

added theorem mul_nonpos_of_nonpos_of_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_le_mul_self_iff

added theorem mul_self_lt_mul_self

added theorem mul_self_lt_mul_self_iff

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

added theorem nonneg_le_nonneg_of_squares_le

added theorem nonneg_of_mul_nonneg_left

added theorem nonneg_of_mul_nonneg_right

modified theorem nonpos_of_mul_nonneg_left

modified theorem nonpos_of_mul_nonneg_right

added theorem nonpos_of_mul_nonpos_left

added theorem nonpos_of_mul_nonpos_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 ordered_ring.mul_le_mul_of_nonneg_left

added theorem ordered_ring.mul_le_mul_of_nonneg_right

added theorem ordered_ring.mul_lt_mul_of_pos_left

added theorem ordered_ring.mul_lt_mul_of_pos_right

added theorem ordered_ring.mul_nonneg

added theorem ordered_semiring.mul_le_mul_of_nonneg_left

added theorem ordered_semiring.mul_le_mul_of_nonneg_right

added theorem pos_and_pos_or_neg_and_neg_of_mul_pos

added theorem pos_of_mul_pos_left

added theorem pos_of_mul_pos_right

added theorem sub_le_of_abs_sub_le_left

added theorem sub_le_of_abs_sub_le_right

added theorem sub_lt_of_abs_sub_lt_left

added theorem sub_lt_of_abs_sub_lt_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

Modified src/algebra/ring.lean

added theorem add_monoid_hom.coe_mul_left

added def add_monoid_hom.mul_left

added def add_monoid_hom.mul_right

added theorem add_monoid_hom.mul_right_apply

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 def dvd_of_mul_left_eq

added theorem dvd_of_mul_right_dvd

added def dvd_of_mul_right_eq

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

modified theorem eq_of_mul_eq_mul_left_of_ne_zero

added theorem eq_of_mul_eq_mul_right

modified theorem eq_of_mul_eq_mul_right_of_ne_zero

modified theorem eq_zero_of_mul_eq_self_left'

added theorem eq_zero_of_mul_eq_self_left

modified theorem eq_zero_of_mul_eq_self_right'

added theorem eq_zero_of_mul_eq_self_right

added theorem eq_zero_of_mul_self_eq_zero

added theorem eq_zero_of_zero_dvd

added theorem eq_zero_or_eq_zero_of_mul_eq_zero

added theorem exists_eq_mul_left_of_dvd

added theorem exists_eq_mul_right_of_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

modified theorem mul_add_eq_mul_add_iff_sub_mul_add_eq

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

added theorem mul_eq_zero_iff_eq_zero_or_eq_zero

modified theorem mul_ne_zero'

added theorem mul_ne_zero

modified theorem mul_ne_zero_comm'

added theorem mul_neg_eq_neg_mul_symm

modified theorem mul_neg_one

added theorem mul_self_eq_mul_self_iff

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_mul_self_eq

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 ne_zero_and_ne_zero_of_mul_ne_zero

added theorem ne_zero_of_mul_ne_zero_left

added theorem ne_zero_of_mul_ne_zero_right

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_eq_neg_mul_symm

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

modified theorem sub_mul_add_eq_of_mul_add_eq_mul_add

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

Modified src/analysis/analytic/basic.lean

Modified src/analysis/complex/polynomial.lean

Modified src/analysis/convex/basic.lean

Modified src/analysis/normed_space/basic.lean

Modified src/analysis/normed_space/real_inner_product.lean

Modified src/control/applicative.lean

deleted theorem comp.applicative_comp_id

deleted theorem comp.applicative_id_comp

deleted theorem comp.map_pure

deleted theorem comp.pure_seq_eq_map

deleted theorem comp.seq_assoc

deleted theorem comp.seq_pure

added theorem functor.comp.applicative_comp_id

added theorem functor.comp.applicative_id_comp

added theorem functor.comp.map_pure

added theorem functor.comp.pure_seq_eq_map

added theorem functor.comp.seq_assoc

added theorem functor.comp.seq_pure

Modified src/control/functor.lean

Modified src/control/monad/writer.lean

Modified src/control/traversable/basic.lean

Modified src/control/traversable/instances.lean

Modified src/control/traversable/lemmas.lean

Modified src/data/array/lemmas.lean

Modified src/data/complex/basic.lean

Modified src/data/complex/exponential.lean

Modified src/data/complex/module.lean

Modified src/data/equiv/basic.lean

Modified src/data/equiv/ring.lean

Modified src/data/equiv/transfer_instance.lean

Modified src/data/fin.lean

Modified src/data/hash_map.lean

Modified src/data/int/basic.lean

Modified src/data/list/basic.lean

Modified src/data/list/defs.lean

Modified src/data/monoid_algebra.lean

Modified src/data/multiset.lean

Modified src/data/nat/basic.lean

added theorem nat.add_units_eq_zero

added theorem nat.units_eq_one

Modified src/data/nat/cast.lean

added theorem nat.inv_pos_of_nat

added theorem nat.one_div_le_one_div

added theorem nat.one_div_lt_one_div

added theorem nat.one_div_pos_of_nat

added theorem with_top.add_one_le_of_lt

added theorem with_top.coe_nat

added theorem with_top.nat_induction

added theorem with_top.nat_ne_top

added theorem with_top.top_ne_nat

Modified src/data/nat/multiplicity.lean

Modified src/data/nat/pairing.lean

Modified src/data/nat/sqrt.lean

Modified src/data/num/lemmas.lean

Modified src/data/padics/hensel.lean

Modified src/data/padics/padic_numbers.lean

Modified src/data/pnat/basic.lean

deleted theorem pnat.dvd_trans

Modified src/data/pnat/xgcd.lean

modified theorem pnat.gcd_eq

Modified src/data/polynomial.lean

Modified src/data/rat/basic.lean

Modified src/data/rat/meta_defs.lean

Modified src/data/real/basic.lean

Modified src/data/real/cau_seq.lean

deleted theorem cau_seq.mul_pos

Modified src/data/real/cau_seq_completion.lean

Modified src/data/seq/computation.lean

Modified src/data/vector2.lean

Modified src/data/zsqrtd/basic.lean

Created src/deprecated/field.lean

added theorem is_ring_hom.injective

added theorem is_ring_hom.map_div

added theorem is_ring_hom.map_eq_zero

added theorem is_ring_hom.map_inv

added theorem is_ring_hom.map_ne_zero

Modified src/deprecated/group.lean

Created src/deprecated/ring.lean

added theorem is_ring_hom.comp

added theorem is_ring_hom.map_neg

added theorem is_ring_hom.map_sub

added theorem is_ring_hom.map_zero

added theorem is_ring_hom.of_semiring

added theorem is_semiring_hom.comp

added theorem ring_hom.coe_of

added def ring_hom.of

Modified src/group_theory/eckmann_hilton.lean

Modified src/group_theory/free_group.lean

Modified src/group_theory/monoid_localization.lean

Modified src/init_/algebra/default.lean

Deleted src/init_/algebra/field.lean

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_div_mul_one_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 division_ring.one_div_mul_one_div

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_mul_eq_mul_of_nonzero_left

deleted theorem eq_of_mul_eq_mul_of_nonzero_right

deleted theorem eq_of_one_div_eq_one_div

deleted theorem eq_one_div_of_mul_eq_one

deleted theorem eq_one_div_of_mul_eq_one_left

deleted theorem eq_zero_of_one_div_eq_zero

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 ne_zero_of_one_div_ne_zero

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_add_mul_one_div_eq_one_div_add_one_div

deleted theorem one_div_mul_cancel

deleted theorem one_div_mul_one_div

deleted theorem one_div_mul_sub_mul_one_div_eq_one_div_add_one_div

deleted theorem one_div_ne_zero

deleted theorem one_div_neg_eq_neg_one_div

deleted theorem one_div_neg_one_eq_neg_one

deleted theorem one_div_one

deleted theorem one_div_one_div

deleted theorem one_inv_eq

deleted theorem zero_div

Deleted src/init_/algebra/functions.lean

deleted theorem abs_abs

deleted theorem abs_abs_sub_abs_le_abs_sub

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_mul_self_add_mul_self_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_le_of_abs_sub_le_right

deleted theorem sub_lt_of_abs_sub_lt_left

deleted theorem sub_lt_of_abs_sub_lt_right

Deleted src/init_/algebra/group.lean

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 def eq_of_add_eq_add_left

deleted def eq_of_add_eq_add_right

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

Modified src/init_/algebra/norm_num.lean

Deleted src/init_/algebra/ordered_field.lean

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_div_of_mul_sub_mul_div_nonpos

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_div_of_mul_sub_mul_div_neg

deleted theorem div_lt_div_of_pos_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_mul_le_div_mul_of_div_le_div_pos'

deleted theorem div_mul_le_div_mul_of_div_le_div_pos

deleted theorem div_neg_of_neg_of_pos

deleted theorem div_neg_of_pos_of_neg

deleted theorem div_nonneg_of_nonneg_of_pos

deleted theorem div_nonneg_of_nonpos_of_neg

deleted theorem div_nonpos_of_nonneg_of_neg

deleted theorem div_nonpos_of_nonpos_of_pos

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 exists_add_lt_and_pos_of_lt

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_div_le_one_div_of_neg

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_div_lt_one_div_of_neg

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 mul_sub_mul_div_mul_nonpos

deleted theorem mul_zero_lt_mul_inv_of_neg

deleted theorem mul_zero_lt_mul_inv_of_pos

deleted theorem neg_of_one_div_neg

deleted theorem one_div_le_neg_one

deleted theorem one_div_le_of_one_div_le_of_neg

deleted theorem one_div_le_of_one_div_le_of_pos

deleted theorem one_div_le_one_div_of_le

deleted theorem one_div_le_one_div_of_le_of_neg

deleted theorem one_div_lt_neg_one

deleted theorem one_div_lt_one_div_of_lt

deleted theorem one_div_lt_one_div_of_lt_of_neg

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 src/init_/algebra/ordered_group.lean

deleted theorem add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg

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 decidable_linear_ordered_add_comm_group.add_lt_add_left

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_add_le_right

deleted theorem le_add_of_neg_le_sub_left

deleted theorem le_add_of_neg_le_sub_right

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_add_lt_right

deleted theorem lt_add_of_neg_lt_sub_left

deleted theorem lt_add_of_neg_lt_sub_right

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_le_right_of_le_add

deleted theorem neg_add_lt_left_of_lt_add

deleted theorem neg_add_lt_of_lt_add

deleted theorem neg_add_lt_right_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_le_sub_right_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_lt_sub_right_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 ordered_add_comm_group.add_lt_add_left

deleted theorem ordered_add_comm_group.le_of_add_le_add_left

deleted theorem ordered_add_comm_group.lt_of_add_lt_add_left

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 src/init_/algebra/ordered_ring.lean

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 linear_ordered_ring.eq_zero_or_eq_zero_of_mul_eq_zero

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_nonneg_right

deleted theorem mul_le_mul_of_nonpos_left

deleted theorem mul_le_mul_of_nonpos_right

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_nonneg_of_nonpos_of_nonpos

deleted theorem mul_nonpos_of_nonneg_of_nonpos

deleted theorem mul_nonpos_of_nonpos_of_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_le_nonneg_of_squares_le

deleted theorem nonneg_of_mul_nonneg_left

deleted theorem nonneg_of_mul_nonneg_right

deleted theorem nonpos_of_mul_nonpos_left

deleted theorem nonpos_of_mul_nonpos_right

deleted theorem ordered_ring.mul_le_mul_of_nonneg_left

deleted theorem ordered_ring.mul_le_mul_of_nonneg_right

deleted theorem ordered_ring.mul_lt_mul_of_pos_left

deleted theorem ordered_ring.mul_lt_mul_of_pos_right

deleted theorem ordered_ring.mul_nonneg

deleted theorem ordered_semiring.mul_le_mul_of_nonneg_left

deleted theorem ordered_semiring.mul_le_mul_of_nonneg_right

deleted theorem pos_and_pos_or_neg_and_neg_of_mul_pos

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 src/init_/algebra/ring.lean

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_mul_eq_self_left

deleted theorem eq_zero_of_mul_eq_self_right

deleted theorem eq_zero_of_mul_self_eq_zero

deleted theorem eq_zero_of_zero_dvd

deleted theorem eq_zero_or_eq_zero_of_mul_eq_zero

deleted theorem exists_eq_mul_left_of_dvd

deleted theorem exists_eq_mul_right_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_eq_zero_iff_eq_zero_or_eq_zero

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 ne_zero_of_mul_ne_zero_left

deleted theorem ne_zero_of_mul_ne_zero_right

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

Modified src/init_/data/int/basic.lean

Modified src/init_/data/int/order.lean

Modified src/init_/data/nat/lemmas.lean

Modified src/linear_algebra/basic.lean

Modified src/linear_algebra/basis.lean

Modified src/linear_algebra/dual.lean

modified def is_basis.coord_fun

Modified src/linear_algebra/multilinear.lean

Modified src/linear_algebra/quadratic_form.lean

Modified src/logic/basic.lean

Modified src/measure_theory/outer_measure.lean

Modified src/number_theory/quadratic_reciprocity.lean

Modified src/number_theory/sum_four_squares.lean

Modified src/order/filter/filter_product.lean

Modified src/ring_theory/integral_domain.lean

Modified src/set_theory/ordinal_notation.lean

Modified src/tactic/abel.lean

Modified src/tactic/algebra.lean

Modified src/tactic/monotonicity/lemmas.lean

Modified src/tactic/norm_num.lean

added theorem norm_num.subst_into_add

added theorem norm_num.subst_into_mul

Modified src/tactic/ring.lean

Modified src/topology/algebra/group.lean

Modified src/topology/algebra/uniform_group.lean

Modified src/topology/bounded_continuous_function.lean

Modified src/topology/metric_space/gromov_hausdorff_realized.lean

Modified src/topology/metric_space/hausdorff_distance.lean

Modified src/topology/metric_space/isometry.lean

Modified test/coinductive.lean

Modified test/finish4.lean

modified def append1

Modified test/library_search/ordered_ring.lean

Modified test/lint.lean

Modified test/lint_simp_comm.lean

Modified test/mk_iff_of_inductive.lean

Modified test/monotonicity.lean

Modified test/norm_cast_int.lean

Modified test/norm_cast_lemma_order.lean

Modified test/norm_num.lean

Modified test/nth_rewrite.lean

Modified test/push_neg.lean

Modified test/refine_struct.lean

Modified test/rewrite.lean

Modified test/ring.lean

Modified test/simp_rw.lean

Modified test/tactics.lean