Theorem smul_finprod

Modification history

2024-09-18 11:42

Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean

feat: add smul_prod lemmas (#8807) …

Deleted smul_finprod View on Github →

2024-08-20 22:47

Mathlib/GroupTheory/GroupAction/BigOperators.lean

feat: monoid action on finprod (#14483)

Added smul_finprod View on Github →