add_monoid_algebra and homogenous
Note that since
direct_sum.has_mul combines indices additively, there is no equivalent to
Main definitions #
add_monoid_algebra.to_direct_sum : add_monoid_algebra M ι → (⨁ i : ι, M)
direct_sum.to_add_monoid_algebra : (⨁ i : ι, M) → add_monoid_algebra M ι
- Bundled equiv versions of the above:
as well as preserving arithmetic operations.
For the bundled equivalences, we provide lemmas that they reduce to
Implementation notes #
This file largely just copies the API of
data/finsupp/to_dfinsupp, and reuses the proofs.
add_monoid_algebra M ι is defeq to
ι →₀ M and
⨁ i : ι, M is defeq to
Π₀ i : ι, M.
Basic definitions and lemmas #
Lemmas about arithmetic operations #
The additive version of
add_monoid_algebra.to_add_monoid_algebra. Note that this is
add_monoid_algebra.has_add is noncomputable.