Commit 2025-07-07 12:10 5e4c8bc4

View on Github →

chore: use typeclass rather than implicit arguments for decidability data (#26662) Additional context available on Zulip Searching with the regex \{.* : Decidable.*\} identifies a handful more such locations but I think they should be dealt with separately (in the first few cases I looked at, the naïve substitution was not sufficient).

Estimated changes

Modified Archive/Wiedijk100Theorems/Partition.lean

modified theorem Theorems100.coeff_indicator

modified theorem Theorems100.coeff_indicator_neg

modified theorem Theorems100.coeff_indicator_pos

modified theorem Theorems100.constantCoeff_indicator

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

modified theorem Finset.prod_apply_dite

modified theorem Finset.prod_apply_ite

modified theorem Finset.prod_apply_ite_of_false

modified theorem Finset.prod_apply_ite_of_true

modified theorem Finset.prod_dite

modified theorem Finset.prod_dite_of_false

modified theorem Finset.prod_dite_of_true

modified theorem Finset.prod_ite

modified theorem Finset.prod_ite_of_false

modified theorem Finset.prod_ite_of_true