Bases for direct sum of modules #
This file defines a Module.Free instance for the direct sum of modules.
Implementation notes #
Currently, to get a basis on ⨁ i, M i from a basis on each M i, use DFinsupp.basis
(using that the types are defeq).
instance
Module.Free.directSum
(R : Type u_1)
[Semiring R]
{ι : Type u_2}
(M : ι → Type u_3)
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → Module R (M i)]
[∀ (i : ι), Free R (M i)]
: