Commit 2024-04-09 03:53 52995972

View on Github →

fix: add missing withOverApps (#12022) This fixes the delaborators for sums, products, infimums, and supremums of pi types and matrices. Also adds a missing whenPPOption getPPNotation to Prefunctor.obj. Zulip thread.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Basic.lean

modified def BigOperators.delabFinsetProd

modified def BigOperators.delabFinsetSum

Modified Mathlib/CategoryTheory/Closed/Cartesian.lean

modified def CategoryTheory.exp.delabPrefunctorObjExp

Modified Mathlib/CategoryTheory/Monoidal/Category.lean

modified def CategoryTheory.MonoidalCategory.delabTensorUnit

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

Modified Mathlib/Order/SetNotation.lean

modified def iInf_delab

modified def iSup_delab