Theorems · Theorem · linear algebra

Submodule.mem_iSup_finset_iff_exists_sum

∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  {s : Finset ι} (p : ι → Submodule R N) (a : N), a ∈ ⨆ i ∈ s, p i ↔ ∃ μ, ∑ i ∈ s, ↑(μ i) = a

Defined in

Mathlib.LinearAlgebra.DFinsupp

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModule