Theorems · Theorem · linear algebra

iSupIndep.dfinsupp_lsum_injective

∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : DecidableEq ι] [inst_1 : Ring R] [inst_2 : AddCommGroup N]
  [inst_3 : Module R N] {p : ι → Submodule R N},
  iSupIndep p → Function.Injective ⇑((DFinsupp.lsum ℕ) fun i => (p i).subtype)

The canonical map out of a direct sum of a family of submodules is injective when the submodules are iSupIndep. Note that this is not generally true for [Semiring R], for instance when A is the ℕ-submodules of the positive and negative integers. See Counterexamples/DirectSumIsInternal.lean for a proof of this fact.

Defined in

Mathlib.LinearAlgebra.DFinsupp

Cited by

5 results in Mathlib

Foundations

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

Assumes

DecidableEqRingAddCommGroupModule