Theorem finsum_smul

Modification history

2026-01-13 19:40

Mathlib/Algebra/BigOperators/Finprod.lean

chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …

Modified finsum_smul View on Github →

2023-08-10 19:52

Mathlib/Algebra/BigOperators/Finprod.lean

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

Modified finsum_smul View on Github →

2023-01-23 14:15

Mathlib/Algebra/BigOperators/Finprod.lean

feat: port Algebra.BigOperators.Finprod (#1766) …

Added finsum_smul View on Github →