Commit 2024-01-19 00:32 b71c5f26

View on Github →

chore: bump Std to leanprover/std4#541 (#9828) Notable changes: lemmas were added in https://github.com/leanprover/std4/pull/538 about gcd and lcm, that now have implicit arguments. Mostly this is a positive change in Mathlib, we can just delete the arguments. The one to consider in review is in ModEq.

Estimated changes

deleted theorem Int.dvd_lcm_left
deleted theorem Int.dvd_lcm_right
deleted theorem Int.gcd_dvd_left
deleted theorem Int.gcd_dvd_right
deleted theorem Int.gcd_neg_left
deleted theorem Int.gcd_neg_right
deleted theorem Int.gcd_one_left
deleted theorem Int.gcd_one_right
deleted def Int.lcm
deleted theorem Int.lcm_self
modified theorem Bool.coe_sort_false
modified theorem Bool.coe_sort_true