Commit 2025-07-19 23:06 6ba59881

View on Github →

feat: remove unnecessary typeclass argument to Finset.prod lemmas for CanonicallyOrderedMul (#27294)

Estimated changes

Modified Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

Modified Mathlib/Data/Finsupp/Weight.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Order.lean

modified theorem hasProd_of_isLUB