Theorem smul_finsum'

Modification history

2026-01-19 09:42

Mathlib/Algebra/BigOperators/Finprod.lean

chore(Algebra): deprecate `DistribMulAction.toAddMonoidHom` (#33724) …

Modified smul_finsum'View on Github →

2025-03-23 00:48

Mathlib/Algebra/BigOperators/Finprod.lean

chore: generalize smul_finsum' from Ring to Monoid (#23224) …

Modified smul_finsum'View on Github →

2023-08-10 19:52

Mathlib/Algebra/BigOperators/Finprod.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified smul_finsum'View on Github →

2023-07-01 11:38

Mathlib/Algebra/BigOperators/Finprod.lean

feat(Algebra/BigOperators/Finprod): variations on `smul_finsum` (#5601) …

Added smul_finsum'View on Github →