Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-04 04:42 5744f897

View on Github →

chore(*): fix some ge_or_gt lint issues (#2945) Also rename a few definitions:

  • ge_of_forall_ge_sub : le_of_forall_sub_le;
  • power_series.order_ge_nat : power_series.nat_le_order;
  • power_series.order_ge: power_series.le_order;

Estimated changes

modified theorem exists_add_lt_and_pos_of_lt
deleted theorem ge_of_forall_ge_sub
added theorem le_of_forall_sub_le
modified theorem abs_nonneg
modified theorem abs_of_nonneg
modified theorem abs_of_pos
modified theorem abs_pos_of_ne_zero
modified theorem abs_pos_of_neg
modified theorem abs_pos_of_pos
modified theorem le_add_of_nonneg_left
modified theorem le_add_of_nonneg_right
modified theorem lt_add_of_pos_left
modified theorem lt_add_of_pos_right
modified theorem sub_le_self
modified theorem sub_lt_self
modified theorem dioph.pell_dioph
modified theorem dioph.xn_dioph
modified theorem pell.d_pos
modified theorem pell.eq_of_xn_modeq'
modified theorem pell.eq_of_xn_modeq
modified theorem pell.eq_of_xn_modeq_le
modified theorem pell.eq_of_xn_modeq_lem3
modified theorem pell.eq_pell_lem
modified theorem pell.eq_pow_of_pell_lem
modified theorem pell.matiyasevic
modified theorem pell.modeq_of_xn_modeq
modified theorem pell.x_pos
modified theorem pell.xy_modeq_of_modeq
added theorem power_series.le_order
deleted theorem power_series.order_add_ge
deleted theorem power_series.order_ge
deleted theorem power_series.order_ge_nat
modified theorem eq_of_forall_dist_le
modified theorem metric.diam_ball
modified theorem metric.diam_closed_ball
modified theorem metric.mem_ball_self
modified theorem metric.mem_closed_ball_self
modified theorem metric.pos_of_mem_ball
modified theorem eq_of_forall_edist_le