Theorem finsum_smul'

Modification history

2023-08-10 19:52

Mathlib/Algebra/BigOperators/Finprod.lean

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

Modified finsum_smul'View on Github →

2023-07-01 11:38

Mathlib/Algebra/BigOperators/Finprod.lean

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

Added finsum_smul'View on Github →