Commit 2025-02-18 17:29 99ac07f6

View on Github →

feat(Algebra/BigOperators/Finprod): add MulEquivClass lemmas (#21638)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Finprod.lean

added theorem MulEquivClass.map_finprod

added theorem map_finset_prod

Modified Mathlib/LinearAlgebra/DFinsupp.lean