Commit 2021-03-29 03:17 f2900006
View on Github →feat(data/equiv/fin): rename sum_fin_sum_equiv to fin_sum_fin_equiv (#6857)
Renames sum_fin_sum_equiv to fin_sum_fin_equiv (as discussed
on Zulip)
Introduces a version with fin(n + m) instead of fin(m + n)
Adds a bunch of simp lemmas for applying these (and their inverses)