Commit 2024-07-30 00:15 9f4987a1

View on Github →

chore(Algebra): remove superfluous DecidableEq hypotheses (#15278) Found by the linter in #10235.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Finsupp.lean

modified theorem Finsupp.prod_mul_eq_prod_mul_of_exists

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

modified theorem Finset.prod_mul_eq_prod_mul_of_exists

Modified Mathlib/Algebra/DirectSum/Basic.lean

modified theorem DirectSum.support_subset