mathlib
3b5a44b8 - chore(src/testing/slim_check/sampleable): simply add explicit namespace `nat.` (#7873)

Commit
4 years ago
chore(src/testing/slim_check/sampleable): simply add explicit namespace `nat.` (#7873) This PR only introduces the explicit namespace `nat.` when calling `le_div_iff_mul_le`. The reason for doing this is that PR #7645 introduces a lemma `le_div_iff_mul_le` in the root namespace and this one then becomes ambiguous. Note that CI *does build* on this branch even without the explicit namespace. The change would only become necessary once/if PR #7645 gets merged. I isolated this change to a separate PR to reduce the diff of #7645 and also to bring attention to this issue, in case someone has some comment about it.
Author
Parents
Loading