Homotopy Type Theory series operator > history (changes)

Showing changes from revision #4 to #5: Added | Removed | Changed

Contents

Definition

Given a $\mathbb{Z}$-module MM and a sequence x:Mx:\mathbb{N} \to M of terms in MM, the series operator

Σ:(M)(M)\Sigma:(\mathbb{N} \to M) \to (\mathbb{N} \to M)

is inductively defined as

Σ(x)(0)x(0)\Sigma(x)(0) \coloneqq x(0)
Σ(x)(i+1)Σ(x)(i)+x(i+1)\Sigma(x)(i + 1) \coloneqq \Sigma(x)(i) + x(i + 1)

for i:i:\mathbb{N}.

Σ(x)\Sigma(x) is called a series.

See also

Last revised on June 17, 2022 at 18:55:58. See the history of this page for a list of all contributions to it.