Commit 2024-09-17 16:36 a5f5e464

View on Github →

chore: Make Finset.prod_product and Fintype.prod_prod_type more uniform (#16884) Make more variables explicit in the rewriting lemmas. Unsimp Fintype.prod_prod_type since Finset.prod_product is not simp.

Estimated changes

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

modified theorem Finset.prod_product'

modified theorem Finset.prod_product

modified theorem Finset.prod_product_right'

modified theorem Finset.prod_product_right

Modified Mathlib/Algebra/MonoidAlgebra/Defs.lean

Modified Mathlib/Data/Fintype/BigOperators.lean

modified theorem Fintype.prod_prod_type'

modified theorem Fintype.prod_prod_type

modified theorem Fintype.prod_prod_type_right'

modified theorem Fintype.prod_prod_type_right

Modified Mathlib/Data/Matrix/Composition.lean

Modified Mathlib/LinearAlgebra/Matrix/Trace.lean

Modified Mathlib/RingTheory/MatrixAlgebra.lean