[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Excluded middle makes everything so much easier since you just work with booleans. Archimedean ordered rational integral domains... Given a commutative ring $R$, we could define the type of power series on $R$ as simply the sequence type $\mathbb{N} \to R$, with power series multiplication defined as convolution of sequences. category: redirected to nlab