Merge branch 'teorth:main' into main

CONTRIBUTING.md

@@ -1,7 +1 @@
-# Contributing to [Project]
-
-Thank you for your interest in contributing to [Project]! We welcome contributions from the
-community and appreciate your efforts to improve the project. Please follow the guidelines below
-to ensure a smooth contribution process.
-
-...
+# Contributing to Equational Theories

README.md

@@ -4,6 +4,8 @@
 
 The purpose of this project is to explore the space of equational theories of magmas, ordered by implication.  To begin with we shall focus only on theories of a single equation, which are listed [here](https://github.com/teorth/equational_theories/blob/main/scripts/equations.txt).
 
+A (manually created) graph of the dependencies obtained so far can be found [here](images/implications.png), current as of Sep 26 2024.
+
 Links:
 
 - [Main web page](https://teorth.github.io/equational_theories/)

blueprint/src/chapter/intro.tex

@@ -3,7 +3,7 @@ \chapter{Introduction}
 \begin{definition}\label{magma-def}\lean{Magma}\leanok A Magma is a set $G$ equipped with a binary operation $\circ: G \times G \to G$.
 \end{definition}
 
-A \emph{law} is a equation involving a finite number of indeterminate variables and the operation $\circ$.  A magma $G$ then obeys that law if the equation holds for all possible choices of indeterminate variables in $G$.  For instance, the commutative law
+A \emph{law} is an equation involving a finite number of indeterminate variables and the operation $\circ$.  A magma $G$ then obeys that law if the equation holds for all possible choices of indeterminate variables in $G$.  For instance, the commutative law
 $$ x \circ y = y \circ x$$
 holds in a magma $G$ if and only if that magma is abelian.
 

home_page/_layouts/default.html

@@ -28,6 +28,7 @@ <h1 class="project-name">{{ page.title | default: site.title | default: site.git
     <h2 class="project-tagline">{{ page.description | default: site.description | default: site.github.project_tagline
       }}</h2>
     <a href="blueprint" class="btn">Blueprint (web)</a>
+    <a href="blueprint.pdf" class="btn">Blueprint (pdf)</a>
     <a href="docs" class="btn">Documentation</a>
     {% if site.github.is_project_page %}
     <a href="{{ site.github.repository_url }}" class="btn">GitHub</a>
@@ -46,4 +47,4 @@ <h2 class="project-tagline">{{ page.description | default: site.description | de
   </main>
 </body>
 
-</html>
+</html>

home_page/index.md

@@ -8,8 +8,8 @@ usemathjax: true
 
 Useful links:
 
-* [Zulip chat for Lean](https://leanprover.zulipchat.com/) for coordination
-* [Blueprint](blueprint/)
-* [Blueprint as pdf](blueprint.pdf)
-* [Dependency graph](blueprint/dep_graph_document.html)
-* [Doc pages for this repository](docs/)
+* [Zulip chat for Lean](https://leanprover.zulipchat.com/#narrow/stream/458659-Equational) for coordination
+* [Blueprint]({{ site.url }}/blueprint/)
+* [Blueprint as pdf]({{ site.url }}/blueprint.pdf)
+* [Dependency graph]({{ site.url }}/blueprint/dep_graph_document.html)
+* [Doc pages for this repository]({{ site.url }}/docs/)