Homotopy Type Theory characteristic > history (Rev #1)

Definition

Let $A$ be a $\mathbb{Z}$-algebra. Let us define the type

where $\cdot$ is the left multiplicative $\mathbb{Z}$-action of $A$. The characteristic of $A$ is defined as

where $\bigwedge$ is the dependent/indexed greatest common divisor function in $\mathbb{N}$.

See also

• Z-algebra