Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-27 07:02 0bc5de53

View on Github →

chore(*): drop some unused args reported by #sanity_check_mathlib (#1490)

  • Drop some unused arguments
  • Drop more unused arguments
  • Move round to the bottom of algebra/archimedean Suggested by @rwbarton

Estimated changes

modified theorem exists_nat_one_div_lt
modified theorem exists_rat_near
modified theorem rat.cast_round
modified theorem associates.dvd_eq_le
modified theorem floor_ring_unique
modified theorem divp_inv
modified theorem with_one.map_eq
modified theorem equiv.symm_trans_swap_trans
modified theorem is_measurable_inl_image
modified theorem is_measurable_inr_image
modified theorem is_measurable_range_inl
modified theorem is_measurable_range_inr
modified theorem pell.eq_of_xn_modeq_lem1
modified theorem polynomial.continuous_eval