Theorems · Theorem · linear algebra

Submodule.iSup_eq_range_dfinsupp_lsum

∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  [inst_3 : DecidableEq ι] (p : ι → Submodule R N), iSup p = ((DFinsupp.lsum ℕ) fun i => (p i).subtype).range

The supremum of a family of submodules is equal to the range of DFinsupp.lsum; that is every element in the iSup can be produced from taking a finite number of non-zero elements of p i, coercing them to N, and summing them.

Defined in

Mathlib.LinearAlgebra.DFinsupp

Cited by

6 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleDecidableEq