Theorems · Theorem · group theory

dfinsuppSumAddHom_mem

∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : AddCommMonoid γ] {S : Type u_1} [inst_3 : SetLike S γ] [AddSubmonoidClass S γ] (s : S) (f : Π₀ (i : ι), β i)
  (g : (i : ι) → β i →+ γ), (∀ (c : ι), f c ≠ 0 → (g c) (f c) ∈ s) → (DFinsupp.sumAddHom g) f ∈ s

Defined in

Mathlib.Data.DFinsupp.Submonoid

Cited by

4 results in Mathlib

Foundations

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

Assumes

DecidableEqAddZeroClassAddCommMonoidSetLikeAddSubmonoidClass