Def PiNotation.delabPi'

Modification history

2023-10-13 21:18
Mathlib/Util/PiNotation.lean
feat: long overdue delaborators (#7633) …
Added PiNotation.delabPi'View on Github →