Theorem Prod.mk.eta

Modification history

2023-09-06 07:39
Mathlib/Data/Prod/Basic.lean
chore: cleanup Mathlib.Init.Data.Prod (#6972) …
Modified Prod.mk.etaView on Github →
2022-11-07 03:20
Mathlib/Data/Prod.lean
feat: port Init.Data.Prod (#543) …
Modified Prod.mk.etaView on Github →
2021-08-03 11:55
Mathlib/Data/Prod.lean
feat(Data/Prod) port data/prod.lean (#28)
Added Prod.mk.etaView on Github →