Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
finite_sum_over_a_monoid [2015/04/17 21:43] nikolaj |
finite_sum_over_a_monoid [2015/04/17 21:44] nikolaj |
||
---|---|---|---|
Line 7: | Line 7: | ||
----- | ----- | ||
+ | === Discussion === | ||
+ | Here $\prod_{S:\mathrm{Sequence}(M)}$ is a dependent function type former. | ||
+ | |||
----- | ----- | ||
=== Context === | === Context === |