Mathlib v3 is deprecated. Go to Mathlib v4

Def equiv.pprod_equiv_prod

Modification history

2021-11-29 17:49
src/data/equiv/basic.lean
chore(*): a few facts about `pprod` (#10519) …
Added equiv.pprod_equiv_prodView on Github →