Def delabProdProjs

Modification history

2024-03-05 18:47
Mathlib/Data/Prod/Basic.lean
chore: update unexpanders (#11165) …
Deleted delabProdProjsView on Github →
2023-10-13 21:18
Mathlib/Data/Prod/Basic.lean
feat: long overdue delaborators (#7633) …
Added delabProdProjsView on Github →