Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-03 19:18 acf5258c

View on Github →

chore(nat/order/basic): remove implicit variables (#17707)

Estimated changes

Modified src/combinatorics/additive/salem_spencer.lean

Modified src/data/nat/order/basic.lean

modified theorem nat.add_eq_max_iff

modified theorem nat.add_eq_min_iff

modified theorem nat.add_mod_eq_ite

modified theorem nat.add_succ_lt_add

modified theorem nat.bit0_le_bit1_iff

modified theorem nat.bit0_lt_bit1_iff

modified theorem nat.bit1_le_bit0_iff

modified theorem nat.bit1_lt_bit0_iff

modified theorem nat.bit_le

modified theorem nat.bit_le_bit1_iff

modified theorem nat.bit_le_bit_iff

modified theorem nat.bit_lt_bit0

modified theorem nat.bit_lt_bit

modified theorem nat.bit_lt_bit_iff

modified theorem nat.div_dvd_of_dvd

modified theorem nat.div_eq_self

modified theorem nat.div_eq_sub_mod_div

modified theorem nat.div_mul_div_comm

modified theorem nat.div_mul_div_le_div

modified theorem nat.eq_one_of_mul_eq_one_left

modified theorem nat.eq_one_of_mul_eq_one_right

modified theorem nat.eq_zero_of_double_le

modified theorem nat.eq_zero_of_le_div

modified theorem nat.eq_zero_of_le_half

modified theorem nat.eq_zero_of_mul_le

modified theorem nat.find_greatest_eq_zero_iff

modified theorem nat.find_greatest_is_greatest

modified theorem nat.find_greatest_mono

modified theorem nat.find_greatest_of_ne_zero

modified theorem nat.find_greatest_spec

modified theorem nat.le_add_one_iff

modified theorem nat.le_and_le_add_one_iff

modified theorem nat.le_find_greatest

modified theorem nat.le_mul_of_pos_left

modified theorem nat.le_mul_of_pos_right

modified theorem nat.le_or_le_of_add_eq_add_pred

modified theorem nat.lt_of_lt_pred

modified theorem nat.lt_pred_iff

modified theorem nat.max_eq_zero_iff

modified theorem nat.min_eq_zero_iff

modified theorem nat.mod_mul_left_div_self

modified theorem nat.mod_mul_right_div_self

modified theorem nat.mul_div_mul_comm_of_dvd_dvd

modified theorem nat.mul_eq_one_iff

modified theorem nat.mul_self_inj

modified theorem nat.mul_self_le_mul_self

modified theorem nat.mul_self_le_mul_self_iff

modified theorem nat.mul_self_lt_mul_self

modified theorem nat.mul_self_lt_mul_self_iff

modified theorem nat.not_dvd_of_between_consec_multiples

modified theorem nat.not_dvd_of_pos_of_lt

modified theorem nat.one_le_iff_ne_zero

modified theorem nat.one_le_of_lt

modified theorem nat.pred_le_iff

modified theorem nat.set_induction_bounded

modified theorem nat.sub_mod_eq_zero_of_mod_eq

modified theorem nat.sub_succ'

modified theorem nat.succ_mul_pos

modified theorem nat.two_mul_odd_div_two

modified theorem nat.zero_max