mathlib

bd835ef5 - feat(logic/equiv/fin): `div`/`mod` as an equivalence on `nat`/`int` (#18359)

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 `n`th term can be collected into an inner / outer sum. We already have the API in most places for `equiv`s and `prod`s 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](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/division.20and.20remainder.20as.20an.20equivalence/near/325359453) Co-authored-by: Junyan Xu <junyanxumath@gmail.com>