Mathlib v3 is deprecated. Go to Mathlib v4

Theorem pprod.mk.eta

Modification history

2021-08-26 11:17
src/data/pprod.lean
refactor(order/filter/bases): allow `ι : Sort*` (#8856) …
Modified pprod.mk.etaView on Github →
2020-11-27 06:39
src/data/pprod.lean
chore(data/pprod): Add pprod.mk.eta (#5114) …
Added pprod.mk.etaView on Github →