Theorems · Theorem · commutative algebra

Finsupp.image_pow_eq_finsuppProd_image

∀ {α : Type u_5} {β : Type u_6} [inst : CommMonoid β] {f : α → β} {n : ℕ} {s : Set α},
  (f '' s) ^ n = (fun x => x.prod fun x1 x2 => f x1 ^ x2) '' {x | Finsupp.degree x = n ∧ ↑x.support ⊆ s}

Defined in

Mathlib.Data.Finsupp.Weight

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoid