Commit 2024-12-20 05:45 1b8a2a51

View on Github →

chore(*): drop some [Decidable*] assumptions (#19988) Found by the linter in #10235

Estimated changes

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

modified theorem Finset.prod_filter_xor

Modified Mathlib/Algebra/BigOperators/Ring.lean

Modified Mathlib/Algebra/MvPolynomial/Degrees.lean

modified theorem MvPolynomial.degreeOf_monomial_eq

Modified Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean

modified theorem CategoryTheory.Limits.Pi.map_eq_prod_map

Modified Mathlib/LinearAlgebra/TensorProduct/Basis.lean