Theorems · Definition · linear algebra

iSupIndep.linearEquiv

{ι : Type u_1} →
  {R : Type u_3} →
    {N : Type u_6} →
      [DecidableEq ι] →
        [inst : Ring R] →
          [inst_1 : AddCommGroup N] →
            [inst_2 : Module R N] → {p : ι → Submodule R N} → iSupIndep p → ⨆ i, p i = ⊤ → (Π₀ (i : ι), ↥(p i)) ≃ₗ[R] N

If (pᵢ)ᵢ is a family of independent submodules that generates the whole module N, then N is isomorphic to the direct sum of the submodules.

Defined in

Mathlib.LinearAlgebra.DFinsupp

Cited by

3 results in Mathlib

Foundations

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

Assumes

DecidableEqRingAddCommGroupModule