Theorems · Theorem · group theory

finsum_mem_mul

∀ {α : Type u_1} {R : Type u_7} [inst : NonUnitalNonAssocSemiring R] [NoZeroDivisors R] {s : Set α} (f : α → R) (r : R),
  (∑ᶠ (a : α) (_ : a ∈ s), f a) * r = ∑ᶠ (a : α) (_ : a ∈ s), f a * r

If R has no zero divisors, then multiplication commutes with finsum_mem. See finsum_mem_mul' for a statement assuming finiteness of support.

Defined in

Mathlib.Algebra.BigOperators.Finprod

Cited by

0 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NonUnitalNonAssocSemiringNoZeroDivisors