Theorems · Theorem · group theory

dfinsuppProd_mem

∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : CommMonoid γ] {S : Type u_1} [inst_4 : SetLike S γ]
  [SubmonoidClass S γ] (s : S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → γ),
  (∀ (c : ι), f c ≠ 0 → g c (f c) ∈ s) → f.prod g ∈ s

Defined in

Mathlib.Data.DFinsupp.Submonoid

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqZeroDecidableCommMonoidSetLikeSubmonoidClass