Theorem MulEquivClass.map_finprod

Modification history

2025-02-18 17:29

Mathlib/Algebra/BigOperators/Finprod.lean

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

Added MulEquivClass.map_finprod View on Github →