Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-06-19 18:19
63c3ab56
View on Github →
chore(data/int/basic): rationalize the arguments implicitness (mostly to_nat_sub_of_le) (
#7997
)
Estimated changes
Modified
src/data/int/basic.lean
modified
theorem
int.coe_pred_of_pos
modified
theorem
int.mod_mod_of_dvd
modified
theorem
int.mul_div_mul_of_pos_left
modified
theorem
int.mul_mod_mul_of_pos
modified
theorem
int.of_nat_add_neg_succ_of_nat_of_lt
modified
theorem
int.sub_div_of_dvd
modified
theorem
int.to_nat_sub_of_le
Modified
src/data/int/modeq.lean