This file defines the direct sum of abelian groups, indexed by a discrete type.
mk β s x is the element of
⨁ i, β i that is zero outside
and has coefficient
x i for
to_group φ is the natural homomorphism from
⨁ i, β i to
induced by a family
φ of homomorphisms
β i → γ.
set_to_set β S T h is the natural homomorphism
⨁ (i : S), β i → ⨁ (i : T), β i,
h : S ⊆ T.
The natural equivalence between
⨁ _ : ι, M and