Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-27 11:55 e0b153b2

View on Github →

refactor(*): drop decidable_linear_order, switch to Lean 3.22.0 (#4762) The main non-bc change in Lean 3.22.0 is leanprover-community/lean#484 which merges linear_order with decidable_linear_order. This is the mathlib part of this PR.

List of API changes

  • All *linear_order* typeclasses now imply decidability of (≤), (<), and (=).
  • Drop classical.DLO.
  • Drop discrete_linear_ordered_field, use linear_ordered_field instead.
  • Drop decidable_linear_ordered_semiring, use linear_ordered_semiring instead.
  • Drop decidable_linear_ordered_comm_ring, use linear_ordered_comm_ring instead;
  • Rename decidable_linear_ordered_cancel_add_comm_monoid to linear_ordered_cancel_add_comm_monoid.
  • Rename decidable_linear_ordered_add_comm_group to linear_ordered_add_comm_group.
  • Modify some lemmas to use weaker typeclass assumptions.
  • Add more lemmas about ordering.compares, including linear_order_of_compares which constructs a linear_order instance from cmp function.

Estimated changes

modified theorem Ico_lemma
modified theorem exists_int_pow_near'
modified theorem exists_int_pow_near
modified theorem finset.abs_sum_le_sum_abs
modified theorem one_lt_fpow
modified theorem abs_neg_one_pow
modified theorem pow_abs
modified theorem cmp_compares
modified theorem ordering.compares.eq_gt
added theorem ordering.compares_swap
added theorem exists_gt_zero
modified theorem fn_min_mul_fn_max
modified theorem min_mul_max
modified theorem units.max_coe
modified theorem units.min_coe
modified theorem abs_two
modified theorem int.cast_abs
modified theorem int.cast_max
modified theorem int.cast_min
modified theorem list.exists_le_of_sum_le
modified theorem list.exists_lt_of_sum_lt
modified theorem multiset.abs_sum_le_sum_abs
modified theorem nat.abs_cast
modified theorem nat.cast_max
modified theorem nat.cast_min
modified theorem rat.cast_abs
modified theorem rat.cast_max
modified theorem rat.cast_min
modified def cau_seq
modified def is_cau_seq
modified theorem hyperreal.coe_abs
modified theorem hyperreal.coe_max
modified theorem hyperreal.coe_min
modified theorem set.Union_Inter_of_monotone
modified theorem function.support_max
modified theorem function.support_min
modified theorem affine_map.image_interval
modified theorem with_bot.coe_le_coe
modified theorem with_bot.inf_eq_min
modified theorem with_bot.lattice_eq_DLO
modified theorem with_bot.some_le_some
modified theorem with_bot.sup_eq_max
modified theorem with_top.inf_eq_min
modified theorem with_top.lattice_eq_DLO
modified theorem with_top.sup_eq_max
modified theorem is_greatest.insert
modified theorem is_greatest.union
modified theorem is_greatest_pair
modified theorem is_least.insert
modified theorem is_least.union
modified theorem is_least_pair
modified theorem filter.germ.abs_def
modified theorem filter.germ.const_abs
modified theorem filter.germ.const_max
modified theorem filter.germ.const_min
modified theorem filter.germ.max_def
modified theorem filter.germ.min_def
modified theorem inf_eq_min
modified theorem sup_eq_max
modified def linear_order_of_STO'
modified theorem summable_abs_iff
modified theorem tendsto_abs_at_top_at_top
modified theorem polynomial.tendsto_infinity
modified theorem cauchy_seq.mem_entourage