From 2ab7c48fba6faf66b58eeb4690c5d0055a9c02a3 Mon Sep 17 00:00:00 2001 From: Vlad Tsyrklevich Date: Fri, 27 Sep 2024 00:49:29 +0200 Subject: [PATCH] Add equations to blueprint --- blueprint/src/chapter/equations.tex | 84 +++++++++++++++++++++++++++++ 1 file changed, 84 insertions(+) diff --git a/blueprint/src/chapter/equations.tex b/blueprint/src/chapter/equations.tex index ecfe596ab..2a0bedcab 100644 --- a/blueprint/src/chapter/equations.tex +++ b/blueprint/src/chapter/equations.tex @@ -24,6 +24,9 @@ \chapter{Equations} \begin{definition}[Equation 8]\label{eq8}\lean{Equation8}\leanok\uses{magma-def} Equation 8 is the law $x=x \circ (x \circ x)$. \end{definition} +\begin{definition}[Equation 23]\label{eq23}\lean{Equation23}\leanok\uses{magma-def} Equation 23 is the law $x = (x \circ x) \circ x$. +\end{definition} + \begin{definition}[Equation 38]\label{eq38}\lean{Equation38}\leanok\uses{magma-def} Equation 38 is the law $x \circ x = x \circ y$. \end{definition} @@ -45,12 +48,93 @@ \chapter{Equations} \begin{definition}[Equation 46]\label{eq46}\lean{Equation46}\leanok\uses{magma-def} Equation 46 is the law $x \circ y = z \circ w$. \end{definition} +\begin{definition}[Equation 47]\label{eq47}\lean{Equation47}\leanok\uses{magma-def} Equation 47 is the law $x = x \circ (x \circ (x \circ x))$. +\end{definition} + +\begin{definition}[Equation 99]\label{eq99}\lean{Equation99}\leanok\uses{magma-def} Equation 99 is the law $x = x \circ ((x \circ x) \circ x)$. +\end{definition} + +\begin{definition}[Equation 151]\label{eq151}\lean{Equation151}\leanok\uses{magma-def} Equation 151 is the law $x = (x \circ x) \circ (x \circ x)$. +\end{definition} + \begin{definition}[Equation 168]\label{eq168}\lean{Equation168}\leanok\uses{magma-def} Equation 168 is the law $x = (y \circ x) \circ (x \circ z)$. \end{definition} +\begin{definition}[Equation 203]\label{eq203}\lean{Equation203}\leanok\uses{magma-def} Equation 203 is the law $x = (x \circ (x \circ x)) \circ x$. +\end{definition} + +\begin{definition}[Equation 255]\label{eq255}\lean{Equation255}\leanok\uses{magma-def} Equation 255 is the law $x = ((x \circ x) \circ x) \circ x$. +\end{definition} + +\begin{definition}[Equation 307]\label{eq307}\lean{Equation307}\leanok\uses{magma-def} Equation 307 is the law $x \circ x = x \circ (x \circ x)$. +\end{definition} + +\begin{definition}[Equation 359]\label{eq359}\lean{Equation359}\leanok\uses{magma-def} Equation 359 is the law $x \circ x = (x \circ x) \circ x$. +\end{definition} + \begin{definition}[Equation 387]\label{eq387}\lean{Equation387}\leanok\uses{magma-def} Equation 387 is the law $x \circ y = (y \circ y) \circ x$. \end{definition} +\begin{definition}[Equation 411]\label{eq411}\lean{Equation411}\leanok\uses{magma-def} Equation 411 is the law $x = x \circ (x \circ (x \circ (x \circ x)))$. +\end{definition} + +\begin{definition}[Equation 614]\label{eq614}\lean{Equation614}\leanok\uses{magma-def} Equation 614 is the law $x = x \circ (x \circ ((x \circ x) \circ x))$. +\end{definition} + +\begin{definition}[Equation 817]\label{eq817}\lean{Equation817}\leanok\uses{magma-def} Equation 817 is the law $x = x \circ ((x \circ x) \circ (x \circ x))$. +\end{definition} + +\begin{definition}[Equation 1020]\label{eq1020}\lean{Equation1020}\leanok\uses{magma-def} Equation 1020 is the law $x = x \circ ((x \circ (x \circ x)) \circ x)$. +\end{definition} + +\begin{definition}[Equation 1223]\label{eq1223}\lean{Equation1223}\leanok\uses{magma-def} Equation 1223 is the law $x = x \circ (((x \circ x) \circ x) \circ x)$. +\end{definition} + +\begin{definition}[Equation 1426]\label{eq1426}\lean{Equation1426}\leanok\uses{magma-def} Equation 1426 is the law $x = (x \circ x) \circ (x \circ (x \circ x))$. +\end{definition} + +\begin{definition}[Equation 1629]\label{eq1629}\lean{Equation1629}\leanok\uses{magma-def} Equation 1629 is the law $x = (x \circ x) \circ ((x \circ x) \circ x)$. +\end{definition} + +\begin{definition}[Equation 1832]\label{eq1832}\lean{Equation1832}\leanok\uses{magma-def} Equation 1832 is the law $x = (x \circ (x \circ x)) \circ (x \circ x)$. +\end{definition} + +\begin{definition}[Equation 2035]\label{eq2035}\lean{Equation2035}\leanok\uses{magma-def} Equation 2035 is the law $x = ((x \circ x) \circ x) \circ (x \circ x)$. +\end{definition} + +\begin{definition}[Equation 2238]\label{eq2238}\lean{Equation2238}\leanok\uses{magma-def} Equation 2238 is the law $x = (x \circ (x \circ (x \circ x))) \circ x$. +\end{definition} + +\begin{definition}[Equation 2441]\label{eq2441}\lean{Equation2441}\leanok\uses{magma-def} Equation 2441 is the law $x = (x \circ ((x \circ x) \circ x)) \circ x$. +\end{definition} + +\begin{definition}[Equation 2644]\label{eq2644}\lean{Equation2644}\leanok\uses{magma-def} Equation 2644 is the law $x = ((x \circ x) \circ (x \circ x)) \circ x$. +\end{definition} + +\begin{definition}[Equation 2847]\label{eq2847}\lean{Equation2847}\leanok\uses{magma-def} Equation 2847 is the law $x = ((x \circ (x \circ x)) \circ x) \circ x$. +\end{definition} + +\begin{definition}[Equation 3050]\label{eq3050}\lean{Equation3050}\leanok\uses{magma-def} Equation 3050 is the law $x = (((x \circ x) \circ x) \circ x) \circ x$. +\end{definition} + +\begin{definition}[Equation 3253]\label{eq3253}\lean{Equation3253}\leanok\uses{magma-def} Equation 3253 is the law $x \circ x = x \circ (x \circ (x \circ x))$. +\end{definition} + +\begin{definition}[Equation 3456]\label{eq3456}\lean{Equation3456}\leanok\uses{magma-def} Equation 3456 is the law $x \circ x = x \circ ((x \circ x) \circ x)$. +\end{definition} + +\begin{definition}[Equation 3659]\label{eq3659}\lean{Equation3659}\leanok\uses{magma-def} Equation 3659 is the law $x \circ x = (x \circ x) \circ (x \circ x)$. +\end{definition} + +\begin{definition}[Equation 3862]\label{eq3862}\lean{Equation3862}\leanok\uses{magma-def} Equation 3862 is the law $x \circ x = (x \circ (x \circ x)) \circ x$. +\end{definition} + +\begin{definition}[Equation 4065]\label{eq4065}\lean{Equation4065}\leanok\uses{magma-def} Equation 4065 is the law $x \circ x = ((x \circ x) \circ x) \circ x$. +\end{definition} + +\begin{definition}[Equation 4380]\label{eq4380}\lean{Equation4380}\leanok\uses{magma-def} Equation 4380 is the law $x \circ (x \circ x) = (x \circ x) \circ x$. +\end{definition} + \begin{definition}[Equation 4512]\label{eq4512}\lean{Equation4512}\leanok\uses{magma-def} Equation 4512 is the law $x \circ (y \circ z) = (x \circ y) \circ z$. \end{definition}