Commit 2024-05-26 11:25 3d14008a
View on Github →feat: More ways of bijecting finsets (#12653)
It is still annoyingly painful to prove that two finsets have equal size by exhibiting a bijection between. This PR remedies this problem by copying over the lemmas that show that two finite sums/products are in bijection. Copy over the names. As a result, rename Finset.card_congr to Finset.card_bij.