mathlib3
56018332 - chore(*): a few facts about `pprod` (#10519)

Commit

4 years ago

chore(*): a few facts about `pprod` (#10519) Add `equiv.pprod_equiv_prod` and `function.embedding.pprod_map`.

Author

urkud

Parents