Commit 2023-02-08 15:26 bd835ef5

feat(logic/equiv/fin): div/mod as an equivalence on nat/int (#18359) The motivation here is to be able to use this to change a sum/product/supr/infi/tsum/etc to be indexed by a product, such that every nth term can be collected into an inner / outer sum. We already have the API in most places for equivs and prods to do this, all that's missing is the equivalences in this PR. Note that we use [ne_zero n] instead of hn : n ≠ 0 as this is required by fin.of_nat' for the coercion. Zulip