Commit 2021-10-08 07:33 eb3595ed

View on Github →

move(order/*): move from algebra.order. the files that aren't about algebra (#9562) algebra.order.basic and algebra.order.functions never mention +, - or *. Thus they belong under order.

Estimated changes

Modified archive/arithcc.lean

Modified src/algebra/covariant_and_contravariant.lean

Deleted src/algebra/order/basic.lean

deleted theorem cmp_compares

deleted theorem cmp_eq_cmp_symm

deleted theorem cmp_eq_eq_iff

deleted theorem cmp_eq_gt_iff

deleted theorem cmp_eq_lt_iff

deleted def cmp_le

deleted theorem cmp_le_eq_cmp

deleted theorem cmp_le_swap

deleted theorem cmp_self_eq_eq

deleted theorem cmp_swap

deleted theorem eq.not_gt

deleted theorem eq.not_lt

deleted theorem eq.trans_le

deleted theorem eq_iff_le_not_lt

deleted theorem eq_of_forall_ge_iff

deleted theorem eq_of_forall_le_iff

deleted theorem eq_or_lt_of_le

deleted theorem exists_ge_of_linear

deleted theorem forall_lt_iff_le'

deleted theorem forall_lt_iff_le

deleted theorem ge_iff_le

deleted theorem ge_of_eq

deleted theorem gt_iff_lt

deleted theorem has_le.le.le_iff_eq

deleted theorem has_le.le.le_or_le

deleted theorem has_le.le.le_or_lt

deleted theorem has_le.le.lt_iff_ne

deleted theorem has_le.le.lt_or_le

deleted theorem has_le.le.trans_eq

deleted theorem has_lt.lt.lt_or_lt

deleted theorem has_lt.lt.ne'

deleted theorem le_iff_eq_or_lt

deleted theorem le_iff_le_iff_lt_iff_lt

deleted theorem le_iff_le_of_cmp_eq_cmp

deleted theorem le_imp_le_iff_lt_imp_lt

deleted theorem le_implies_le_of_le_of_le

deleted theorem le_of_forall_le'

deleted theorem le_of_forall_le

deleted theorem le_of_forall_lt'

deleted theorem le_of_forall_lt

deleted theorem le_rfl

deleted def linear_order_of_compares

deleted theorem lt_iff_le_and_ne

deleted theorem lt_iff_lt_of_cmp_eq_cmp

deleted theorem lt_iff_lt_of_le_iff_le'

deleted theorem lt_iff_lt_of_le_iff_le

deleted theorem lt_iff_not_ge'

deleted theorem lt_imp_lt_of_le_imp_le

deleted theorem lt_of_not_ge'

deleted theorem ne.le_iff_lt

deleted theorem ne.lt_or_lt

deleted theorem ne_iff_lt_iff_le

deleted theorem not_le_of_lt

deleted theorem not_lt_iff_eq_or_lt

deleted theorem not_lt_of_le

deleted theorem ordering.compares.eq_eq

deleted theorem ordering.compares.eq_gt

deleted theorem ordering.compares.eq_lt

deleted theorem ordering.compares.inj

deleted theorem ordering.compares.le_antisymm

deleted theorem ordering.compares.le_total

deleted theorem ordering.compares.ne_gt

deleted theorem ordering.compares.ne_lt

deleted def ordering.compares

deleted theorem ordering.compares_iff_of_compares_impl

deleted theorem ordering.compares_swap

deleted theorem ordering.or_else_eq_lt

deleted theorem ordering.swap_eq_iff_eq_swap

deleted theorem ordering.swap_or_else

Modified src/algebra/order/monoid.lean

Modified src/computability/turing_machine.lean

Modified src/data/int/basic.lean

Modified src/order/basic.lean

added theorem eq.not_gt

added theorem eq.not_lt

added theorem eq.trans_le

added theorem eq_iff_le_not_lt

added theorem eq_of_forall_ge_iff

added theorem eq_of_forall_le_iff

added theorem eq_or_lt_of_le

added theorem exists_ge_of_linear

added theorem forall_lt_iff_le'

added theorem forall_lt_iff_le

added theorem ge_iff_le

added theorem ge_of_eq

added theorem gt_iff_lt

added theorem has_le.le.le_iff_eq

added theorem has_le.le.le_or_le

added theorem has_le.le.le_or_lt

added theorem has_le.le.lt_iff_ne

added theorem has_le.le.lt_or_le

added theorem has_le.le.trans_eq

added theorem has_lt.lt.lt_or_lt

added theorem has_lt.lt.ne'

added theorem le_iff_eq_or_lt

added theorem le_iff_le_iff_lt_iff_lt

added theorem le_imp_le_iff_lt_imp_lt

added theorem le_implies_le_of_le_of_le

added theorem le_of_forall_le'

added theorem le_of_forall_le

added theorem le_of_forall_lt'

added theorem le_of_forall_lt

added theorem le_rfl

added theorem lt_iff_le_and_ne

added theorem lt_iff_lt_of_le_iff_le'

added theorem lt_iff_lt_of_le_iff_le

added theorem lt_iff_not_ge'

added theorem lt_imp_lt_of_le_imp_le

added theorem lt_of_not_ge'

modified theorem lt_self_iff_false

added theorem ne.le_iff_lt

added theorem ne.lt_or_lt

added theorem ne_iff_lt_iff_le

added theorem not_le_of_lt

added theorem not_lt_iff_eq_or_lt

added theorem not_lt_of_le

deleted theorem order_dual.cmp_le_flip

deleted theorem order_dual.dual_compares

Created src/order/compare.lean

added theorem cmp_compares

added theorem cmp_eq_cmp_symm

added theorem cmp_eq_eq_iff

added theorem cmp_eq_gt_iff

added theorem cmp_eq_lt_iff

added def cmp_le

added theorem cmp_le_eq_cmp

added theorem cmp_le_swap

added theorem cmp_self_eq_eq

added theorem cmp_swap

added theorem le_iff_le_of_cmp_eq_cmp

added def linear_order_of_compares

added theorem lt_iff_lt_of_cmp_eq_cmp

added theorem order_dual.cmp_le_flip

added theorem order_dual.dual_compares

added theorem ordering.compares.eq_eq

added theorem ordering.compares.eq_gt

added theorem ordering.compares.eq_lt

added theorem ordering.compares.inj

added theorem ordering.compares.le_antisymm

added theorem ordering.compares.le_total

added theorem ordering.compares.ne_gt

added theorem ordering.compares.ne_lt

added def ordering.compares

added theorem ordering.compares_iff_of_compares_impl

added theorem ordering.compares_swap

added theorem ordering.or_else_eq_lt

added theorem ordering.swap_eq_iff_eq_swap

added theorem ordering.swap_or_else

Renamed src/algebra/order/functions.lean to src/order/min_max.lean

Modified src/order/monotone.lean

Modified src/order/pilex.lean

Modified src/tactic/push_neg.lean