Theorems · Theorem · ring theory

TwoSidedIdeal.dfinsuppSum_mem

∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {ι : Type u_2} {β : ι → Type u_3}
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → Zero (β i)] [inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)]
  {f : Π₀ (i : ι), β i} (g : (i : ι) → β i → R), (∀ i ∈ f.support, g i (f i) ∈ I) → f.sum g ∈ I

Defined in

Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonUnitalNonAssocRingDecidableEqZeroDecidable