Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-13 11:47 02b85de4

View on Github →

chore(algebra/order/sub): split file (#16868)

depends on: #16861

Estimated changes

Renamed src/algebra/order/group.lean to src/algebra/order/group/basic.lean

Created src/algebra/order/group/type_tags.lean

Modified src/algebra/order/lattice_group.lean

Modified src/algebra/order/monoid/canonical.lean

Modified src/algebra/order/ring.lean

Created src/algebra/order/sub/basic.lean

added theorem add_hom.le_map_tsub

added theorem add_le_add_add_tsub

added theorem add_monoid_hom.le_map_tsub

added theorem add_tsub_add_eq_tsub_left

added theorem add_tsub_add_eq_tsub_right

added theorem add_tsub_add_le_tsub_add_tsub

added theorem add_tsub_add_le_tsub_left

added theorem add_tsub_add_le_tsub_right

added theorem add_tsub_cancel_left

added theorem add_tsub_cancel_right

added theorem add_tsub_le_assoc

added theorem add_tsub_le_left

added theorem add_tsub_le_right

added theorem add_tsub_le_tsub_add

added theorem antitone_const_tsub

added theorem eq_tsub_of_add_eq

added theorem le_add_tsub'

added theorem le_add_tsub

added theorem le_add_tsub_swap

added theorem le_mul_tsub

added theorem le_tsub_add

added theorem le_tsub_add_add

added theorem le_tsub_mul

added theorem le_tsub_of_add_le_left

added theorem le_tsub_of_add_le_right

added theorem lt_add_of_tsub_lt_left

added theorem lt_add_of_tsub_lt_right

added theorem lt_of_tsub_lt_tsub_left

added theorem lt_of_tsub_lt_tsub_right

added theorem lt_tsub_comm

added theorem lt_tsub_iff_left

added theorem lt_tsub_iff_right

added theorem lt_tsub_of_add_lt_left

added theorem lt_tsub_of_add_lt_right

added theorem order_iso.map_tsub

added theorem tsub_add_eq_tsub_tsub

added theorem tsub_add_eq_tsub_tsub_swap

added theorem tsub_eq_of_eq_add

added theorem tsub_eq_of_eq_add_rev

added theorem tsub_le_iff_left

added theorem tsub_le_iff_right

added theorem tsub_le_iff_tsub_le

added theorem tsub_le_tsub

added theorem tsub_le_tsub_add_tsub

added theorem tsub_le_tsub_left

added theorem tsub_le_tsub_right

added theorem tsub_nonpos

added theorem tsub_right_comm

added theorem tsub_tsub

added theorem tsub_tsub_le

added theorem tsub_tsub_le_tsub_add

added theorem tsub_tsub_tsub_le_tsub

added theorem tsub_zero

Renamed src/algebra/order/sub.lean to src/algebra/order/sub/canonical.lean

deleted theorem add_hom.le_map_tsub

deleted theorem add_le_add_add_tsub

deleted theorem add_monoid_hom.le_map_tsub

deleted theorem add_tsub_add_eq_tsub_left

deleted theorem add_tsub_add_eq_tsub_right

deleted theorem add_tsub_add_le_tsub_add_tsub

deleted theorem add_tsub_add_le_tsub_left

deleted theorem add_tsub_add_le_tsub_right

deleted theorem add_tsub_cancel_left

deleted theorem add_tsub_cancel_right

deleted theorem add_tsub_le_assoc

deleted theorem add_tsub_le_left

deleted theorem add_tsub_le_right

deleted theorem add_tsub_le_tsub_add

deleted theorem antitone_const_tsub

deleted theorem eq_tsub_of_add_eq

deleted theorem le_add_tsub'

deleted theorem le_add_tsub

deleted theorem le_add_tsub_swap

deleted theorem le_mul_tsub

deleted theorem le_tsub_add

deleted theorem le_tsub_add_add

deleted theorem le_tsub_mul

deleted theorem le_tsub_of_add_le_left

deleted theorem le_tsub_of_add_le_right

deleted theorem lt_add_of_tsub_lt_left

deleted theorem lt_add_of_tsub_lt_right

deleted theorem lt_of_tsub_lt_tsub_left

deleted theorem lt_of_tsub_lt_tsub_right

deleted theorem lt_tsub_comm

deleted theorem lt_tsub_iff_left

deleted theorem lt_tsub_iff_right

deleted theorem lt_tsub_of_add_lt_left

deleted theorem lt_tsub_of_add_lt_right

deleted theorem order_iso.map_tsub

deleted theorem tsub_add_eq_tsub_tsub

deleted theorem tsub_add_eq_tsub_tsub_swap

deleted theorem tsub_eq_of_eq_add

deleted theorem tsub_eq_of_eq_add_rev

deleted theorem tsub_le_iff_left

deleted theorem tsub_le_iff_right

deleted theorem tsub_le_iff_tsub_le

deleted theorem tsub_le_tsub

deleted theorem tsub_le_tsub_add_tsub

deleted theorem tsub_le_tsub_left

deleted theorem tsub_le_tsub_right

deleted theorem tsub_nonpos

deleted theorem tsub_right_comm

deleted theorem tsub_tsub

deleted theorem tsub_tsub_le

deleted theorem tsub_tsub_le_tsub_add

deleted theorem tsub_tsub_tsub_le_tsub

deleted theorem tsub_zero

deleted theorem with_top.coe_sub

deleted theorem with_top.sub_top

deleted theorem with_top.top_sub_coe

Created src/algebra/order/sub/with_top.lean

added theorem with_top.coe_sub

added theorem with_top.sub_top

added theorem with_top.top_sub_coe

Modified src/algebra/order/with_zero.lean

Modified src/data/nat/enat.lean

Modified src/data/nat/with_bot.lean

Modified src/data/real/ennreal.lean

Modified src/data/set/intervals/basic.lean