Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-27 06:39 d3cc9935

View on Github →

chore(data/pprod): Add pprod.mk.eta (#5114) This is exactly the same as prod.mk.eta

Estimated changes

added theorem pprod.mk.eta