LeanPool.BrauerGroupNew.Mathlib.Data.DFinsupp.Submonoid #
Imported Lean Pool material for LeanPool.BrauerGroupNew.Mathlib.Data.DFinsupp.Submonoid.
theorem
finsuppProd_mem
{ι : Type u_1}
{γ : Type u_2}
{β : Type u_3}
[Zero β]
[CommMonoid γ]
{S : Type u_4}
[SetLike S γ]
[SubmonoidClass S γ]
{s : S}
{f : ι →₀ β}
{g : ι → β → γ}
(h : ∀ (c : ι), f c ≠ 0 → g c (f c) ∈ s)
:
theorem
finsuppSum_mem
{ι : Type u_1}
{γ : Type u_2}
{β : Type u_3}
[Zero β]
[AddCommMonoid γ]
{S : Type u_4}
[SetLike S γ]
[AddSubmonoidClass S γ]
{s : S}
{f : ι →₀ β}
{g : ι → β → γ}
(h : ∀ (c : ι), f c ≠ 0 → g c (f c) ∈ s)
: