card): generalize `equiv.prod_comp` to `function.bijective.prod_comp` (#5551)

Commit

5 years ago

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`.

Author

urkud

Parents

ea3815fb

mathlib3 06a11fd5 - chore(data/fintype/card): generalize `equiv.prod_comp` to `function.bijective.prod_comp` (#5551)

mathlib3
06a11fd5 - chore(data/fintype/card): generalize `equiv.prod_comp` to `function.bijective.prod_comp` (#5551)