Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-14 05:00 81a31ca4

View on Github →

chore(data/*): flipping inequalities (#1436)

  • chore(data/*): flipping inequalities
  • some more
  • Update src/algebra/order_functions.lean
  • fixing some names
  • fix
  • fixes
  • fixes
  • making names/comments uniform
  • fixes
  • fixes
  • fix
  • rename
  • fixes
  • fixes
  • fix
  • renames
  • I'm so bad at this
  • ...
  • fixes

Estimated changes

deleted theorem pow_unbounded_of_gt_one
deleted theorem fpow_ge_one_of_nonneg
modified theorem fpow_le_one_of_nonpos
modified theorem fpow_nonneg_of_nonneg
modified theorem fpow_pos_of_pos
added theorem one_le_fpow_of_nonneg
modified theorem one_lt_fpow
modified theorem one_lt_pow
modified theorem pow_le_max_of_min_le
modified theorem ceil_nonneg
modified theorem add_monoid.smul_sub
added theorem one_add_mul_le_pow
added theorem one_add_sub_mul_le_pow
deleted theorem pow_ge_one_add_mul
deleted theorem pow_ge_one_add_sub_mul
modified theorem pow_sub
modified theorem decidable.ne_iff_lt_or_gt
modified theorem abs_eq
modified theorem le_add_of_nonneg_left'
modified theorem le_add_of_nonneg_right'
modified theorem le_mul_iff_one_le_left
modified theorem le_mul_iff_one_le_right
deleted theorem le_mul_of_ge_one_left'
deleted theorem le_mul_of_ge_one_right'
added theorem le_mul_of_one_le_left'
modified theorem lt_mul_iff_one_lt_left
modified theorem lt_mul_iff_one_lt_right
deleted theorem lt_mul_of_gt_one_right'
modified theorem mul_le_iff_le_one_left
modified theorem mul_le_iff_le_one_right
modified theorem mul_lt_iff_lt_one_left
modified theorem mul_lt_iff_lt_one_right
added theorem mul_nonneg'
added theorem mul_pos'
deleted theorem zero_le_mul
modified theorem fin.add_nat_val
modified def fin.sub_nat
modified theorem fin.sub_nat_val
deleted theorem finset.Ico.filter_ge
added theorem finset.Ico.filter_le
modified theorem finset.Ico.pred_singleton
modified theorem int.div_le_self
modified theorem int.div_neg'
modified theorem int.div_of_neg_of_pos
modified theorem int.div_pos_of_pos_of_dvd
modified theorem int.dvd_antisymm
modified theorem int.eq_one_of_dvd_one
modified theorem int.le_of_dvd
modified theorem int.lt_div_add_one_mul_self
modified theorem int.mod_lt_of_pos
modified theorem int.mod_nonneg
modified theorem int.mul_div_mul_of_pos
modified theorem int.mul_div_mul_of_pos_left
modified theorem int.mul_mod_mul_of_pos
modified theorem int.neg_succ_of_nat_div
modified theorem int.neg_succ_of_nat_mod
deleted theorem list.Ico.filter_ge
deleted theorem list.Ico.filter_ge_of_ge
added theorem list.Ico.filter_le
modified theorem list.Ico.pred_singleton
deleted theorem list.nth_ge_len
added theorem list.nth_len_le
deleted theorem list.take_all_of_ge
added theorem list.take_all_of_le
deleted theorem multiset.Ico.filter_ge
added theorem multiset.Ico.filter_le
modified theorem multiset.Ico.pred_singleton
modified theorem nat.add_pos_iff_pos_or_pos
modified theorem nat.add_pos_left
modified theorem nat.add_pos_right
modified theorem nat.dvd_fact
modified theorem nat.fact_pos
modified theorem nat.le_induction
modified theorem nat.le_mul_of_pos_left
modified theorem nat.le_mul_of_pos_right
modified theorem nat.lt_pow_self
modified theorem nat.not_pos_pow_dvd
modified theorem nat.pos_iff_ne_zero
modified theorem nat.pow_lt_pow_succ
modified theorem nat.pow_pos
modified theorem nat.cast_pred
modified theorem nat.dist_pos_of_ne
modified theorem nat.coprime_div_gcd_div_gcd
modified theorem nat.coprime_of_dvd
modified theorem nat.exists_coprime'
modified theorem nat.exists_coprime
modified theorem nat.gcd_le_left
modified theorem nat.gcd_le_right
modified theorem nat.gcd_pos_of_pos_left
modified theorem nat.gcd_pos_of_pos_right
modified theorem nat.unpair_lt
modified theorem nat.even_sub
deleted theorem nat.dvd_prime_ge_two
added theorem nat.dvd_prime_two_le
modified theorem nat.exists_dvd_of_not_prime
modified theorem nat.exists_infinite_primes
modified theorem nat.exists_prime_and_dvd
modified theorem nat.min_fac_aux_has_prop
modified theorem nat.min_fac_le
modified theorem nat.min_fac_le_of_dvd
modified theorem nat.min_fac_pos
deleted theorem nat.prime.ge_two
deleted theorem nat.prime.gt_one
added theorem nat.prime.one_lt
modified theorem nat.prime.pos
modified theorem nat.prime.pred_pos
added theorem nat.prime.two_le
modified def nat.prime
modified theorem nat.prime_def_le_sqrt
modified theorem nat.prime_def_lt'
modified theorem nat.prime_def_lt
modified theorem nat.prime_def_min_fac
modified theorem nat.sqrt_lt_self
modified theorem nat.sqrt_pos
modified theorem pos_num.cast_pos
modified theorem pos_num.to_nat_pos
modified def nat.to_pnat
modified theorem pnat.pos
modified theorem pnat.sub_coe
modified theorem pnat.to_pnat'_coe
modified def pnat
modified theorem rat.mk_nonneg
modified theorem zsqrtd.not_sq_le_succ