Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-15 20:42 b97b08b7

View on Github →

fix(*): remove usages of ge/gt (#3808) These were not caught by the old ge_or_gt linter, but they will be caught by the new (upcoming) ge_or_gt linter. The nolint flags are not yet removed, this will happen in a later PR. Renamings:

char_is_prime_of_ge_two -> char_is_prime_of_two_le
dist_eq_sub_of_ge -> dist_eq_sub_of_le_right
gt_of_mul_lt_mul_neg_right -> lt_of_mul_lt_mul_neg_right

Estimated changes

modified theorem max_le_add_of_nonneg
modified theorem min_le_add_of_nonneg_left
modified theorem min_le_add_of_nonneg_right
modified theorem nat.eq_of_mul_eq_mul_right
deleted theorem nat.dist_eq_sub_of_ge
modified theorem num.cmp_to_nat
modified theorem pos_num.cmp_to_nat
modified theorem pos_num.pred_to_nat
modified theorem znum.cmp_to_int
modified theorem padic.padic_norm_e_lim_le
modified theorem padic.rat_dense'
modified theorem padic.rat_dense
modified theorem padic_norm_e.defn
modified theorem padic_seq.norm_nonneg
modified theorem cau_seq.cauchy₂
modified theorem cau_seq.cauchy₃
modified theorem is_cau_seq.cauchy₂
modified theorem is_cau_seq.cauchy₃
modified theorem hyperreal.infinite_pos_def
modified theorem ordinal.add_absorp_iff
modified theorem linarith.mul_eq
modified theorem linarith.mul_neg
modified theorem linarith.mul_nonpos
modified theorem gt_mem_sets_of_Liminf_gt