[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] \tableofcontents Laterally, across Integers, rings, finite-dimensional Clifford rings $\mathrm{Cl}_{p, q}(\mathbb{Z})$ Commutative rings, $R$-algebras, finite-dimensional $R$-Clifford algebras $\mathrm{Cl}_{p, q}(R)$ Rational number field, rational algebras, finite-dimensional rational Clifford algebras $\mathrm{Cl}_{p, q}(\mathbb{Q})$ Real number fields, real algebras, finite-dimensional real Clifford algebras $\mathrm{Cl}_{p, q}(\mathbb{R})$ \section{Ordered commutative ring} ... \section{Ordered field} An ordered field is an ordered commutative ring such that every element which is greater than or less than zero is invertible. \section{Euclidean field} A Euclidean field is an ordered field where the square function, restricted to the non-negative elements, has a retract. Every Euclidean field has an absolute value function given by $\vert x \vert \coloneqq \sqrt{x^2}$ and a pseudolattice structure given by $\min(x, y) = \frac{x + y - \vert y - x \vert}{2}$, $\max(x, y) = \frac{x + y + \vert y - x \vert}{2}$ \section{Archimedean Euclidean field} ... \section{Real number field} A real number field is a sequentially Cauchy complete Archimedean Euclidean field. \section{Quadratic closures} A field is **quadratically closed** if every non-degenerate monic quadratic function is the product of two monic affine functions. Quadratic closure: Every non-degenerate monic quadratic function is the product of two monic affine functions. \section{Test} Literal basic stuff about high school algebra: * What is a variable? * What are free and bound variables? * What is substitution of terms for variables? \section{Variables} A variable is a symbol $x$ which represents an arbitrary instantiation of a type $T$. Variables are thus types and written as $x:T$. Variables are usually found in the context, as $\Gamma, x:T, \Delta \vdash \mathcal{J}$ for arbitrary judgment $\mathcal{J}$. \section{Free and bound variables} \section{Substitution} \section{Change of bound variables} category: redirected to nlab