Theorems · Definition · linear algebra

DFinsupp.basis

{ι : Type u_1} →
  {R : Type u_2} →
    {M : ι → Type u_3} →
      [inst : Semiring R] →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] →
            {η : ι → Type u_4} →
              ((i : ι) → Module.Basis (η i) R (M i)) → Module.Basis ((i : ι) × η i) R (Π₀ (i : ι), M i)

The direct sum of free modules is free. Note that while this is stated for DFinsupp not DirectSum, the types are defeq.

Defined in

Mathlib.LinearAlgebra.Finsupp.VectorSpace

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModule