## Euclidean semirings ## Given a additively cancellative commutative semiring $R$, a term $e:R$ is *left cancellative* if for all $a:R$ and $b:R$, $e \cdot a = e \cdot b$ implies $a = b$. $$\mathrm{isLeftCancellative}(e) \coloneqq \prod_{a:R} \prod_{b :R}(e \cdot a = e \cdot b) \to (a = b)$$ A term $e:R$ is *right cancellative* if for all $a:R$ and $b:R$, $a \cdot e = b \cdot e$ implies $a = b$. $$\mathrm{isRightCancellative}(e) \coloneqq \prod_{a:R} \prod_{b :R}(a \cdot e = b \cdot e) \to (a = b)$$ An term $e:R$ is *cancellative* if it is both left cancellative and right cancellative. $$\mathrm{isCancellative}(e) \coloneqq \mathrm{isLeftCancellative}(e) \times \mathrm{isRightCancellative}(e)$$ The **multiplicative submonoid of cancellative elements in $R$** is the subset of all cancellative elements in $R$ $$\mathrm{Can}(R) \coloneqq \sum_{e:R} \mathrm{isCancellative}(e)$$ A **Euclidean semiring** is a additively cancellative commutative semiring $R$ for which there exists a function $d \colon \mathrm{Can}(R) \to \mathbb{N}$ from the multiplicative submonoid of cancellative elements in $R$ to the [[natural numbers]], often called a *degree function*, a function $(-)\div(-):R \times \mathrm{Can}(R) \to R$ called the *division function*, and a function $(-)\ \%\ (-):R \times \mathrm{Can}(R) \to R$ called the remainder function, such that for all $a \in R$ and $b \in \mathrm{Can}(R)$, $a = (a \div b) \cdot b + (a\ \%\ b)$ and either $a\ \%\ b = 0$ or $d(a\ \%\ b) \lt d(g)$.