Commit 2023-02-08 15:26 bd835ef5
View on Github →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