Theorems · Theorem · commutative algebra

DividedPowerAlgebra.dp_sum

∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : DecidableEq ι] (s : Finset ι) (q : ℕ) (x : ι → M),
  DividedPowerAlgebra.dp R q (s.sum x) = ∑ k ∈ s.sym q, ∏ i ∈ s, DividedPowerAlgebra.dp R (Multiset.count i ↑k) (x i)

Defined in

Mathlib.RingTheory.DividedPowerAlgebra.Init

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleDecidableEq