Commit 2021-01-02 00:36 06a11fd5

chore(data/fintype/card): generalize equiv.prod_comp to function.bijective.prod_comp (#5551) This way we can apply it to add_equiv, mul_equiv, order_iso, etc without using to_equiv.