Commit 2023-07-31 15:32 4ada7e3d

View on Github →

feat(Algebra/BigOperators/Ring): parameterise DecidableEq instance for Finset.prod_add (#5798) Remove the use of a classical DecidableEq instance from Finset.prod_add.

Estimated changes

modified theorem Finset.prod_add