Merge pull request #17 from carlini/typo-4552

Correct typo: Equation4522 is sometimes called Equation 4552

blueprint/src/chapter/counterexamples.tex

@@ -55,7 +55,7 @@ \chapter{Counterexamples}
 \begin{proof}\leanok Use the natural numbers $\N$ with operation $x \circ y := x \cdot y + 1$.
 \end{proof}
 
-\begin{theorem}[4513 does not imply 4552]\label{4513_not_imply_4552}\lean{Equation4513_not_implies_Equation4552}\leanok\uses{eq4513,eq4552} Definition \ref{eq4513} does not imply Definition \ref{eq4552}.
+\begin{theorem}[4513 does not imply 4522]\label{4513_not_imply_4522}\lean{Equation4513_not_implies_Equation4522}\leanok\uses{eq4513,eq4522} Definition \ref{eq4513} does not imply Definition \ref{eq4522}.
 \end{theorem}
 
 \begin{proof}\leanok Use the natural numbers $\N$ with operation $x \circ y$ equal to $1$ if $x=0$ and $y \leq 2$, $2$ if $x=0$ and $y>2$, and $x$ otherwise.

blueprint/src/chapter/equations.tex

@@ -57,7 +57,7 @@ \chapter{Equations}
 \begin{definition}[Equation 4513]\label{eq4513}\lean{Equation4513}\leanok\uses{magma-def}  Equation 4513 is the law $x \circ (y \circ z) = (x \circ y) \circ w$.
 \end{definition}
 
-\begin{definition}[Equation 4552]\label{eq4552}\lean{Equation4552}\leanok\uses{magma-def}  Equation 4552 is the law $x \circ (y \circ z) = (x \circ w) \circ u$.
+\begin{definition}[Equation 4522]\label{eq4522}\lean{Equation4522}\leanok\uses{magma-def}  Equation 4522 is the law $x \circ (y \circ z) = (x \circ w) \circ u$.
 \end{definition}
 
 \begin{definition}[Equation 4582]\label{eq4582}\lean{Equation4582}\leanok\uses{magma-def}  Equation 4582 is the law $x \circ (y \circ z) = (w \circ u) \circ v$.

equational_theories/Basic.lean

@@ -67,7 +67,7 @@ def Equation4512 (G: Type*) [Magma G] := ∀ x y z : G, x ∘ (y ∘ z) = (x ∘
 
 def Equation4513 (G: Type*) [Magma G] := ∀ x y z w : G, x ∘ (y ∘ z) = (x ∘ y) ∘ w
 
-def Equation4552 (G: Type*) [Magma G] := ∀ x y z w u : G, x ∘ (y ∘ z) = (x ∘ w) ∘ u
+def Equation4522 (G: Type*) [Magma G] := ∀ x y z w u : G, x ∘ (y ∘ z) = (x ∘ w) ∘ u
 
 /-- all products of three values are the same, regardless bracketing -/
 def Equation4582 (G: Type*) [Magma G] := ∀ x y z w u v: G, x ∘ (y ∘ z) = (w ∘ u) ∘ v
@@ -106,7 +106,7 @@ theorem Equation4_implies_Equation42 (G: Type*) [Magma G] (h: Equation4 G) : Equ
   intro _ _ _
   rw [<-h, <-h]
 
-theorem Equation4_implies_Equation4552 (G: Type*) [Magma G] (h: Equation4 G) : Equation4552 G := by
+theorem Equation4_implies_Equation4522 (G: Type*) [Magma G] (h: Equation4 G) : Equation4522 G := by
   intro x y z w u
   rw [<-h, <-h, <-h]
 
@@ -133,10 +133,10 @@ theorem Equation387_implies_Equation43 (G: Type*) [Magma G] (h: Equation387 G) :
 theorem Equation4513_implies_Equation4512 (G: Type*) [Magma G] (h: Equation4513 G) : Equation4512 G :=
   fun _ _ _ => h _ _ _ _
 
-theorem Equation4552_implies_Equation4513 (G: Type*) [Magma G] (h: Equation4552 G) : Equation4513 G :=
+theorem Equation4522_implies_Equation4513 (G: Type*) [Magma G] (h: Equation4522 G) : Equation4513 G :=
   fun _ _ _ _ => h _ _ _ _ _
 
-theorem Equation4582_implies_Equation4552 (G: Type*) [Magma G] (h: Equation4582 G) : Equation4552 G :=
+theorem Equation4582_implies_Equation4522 (G: Type*) [Magma G] (h: Equation4582 G) : Equation4522 G :=
   fun _ _ _ _ _ => h _ _ _ _ _ _
 
 
@@ -348,7 +348,7 @@ theorem Equation4512_not_implies_Equation4513 : ∃ (G: Type) (_: Magma G), Equa
   dsimp [hG] at h
   linarith
 
-theorem Equation4513_not_implies_Equation4552 : ∃ (G: Type) (_: Magma G), Equation4513 G ∧ ¬ Equation4552 G := by
+theorem Equation4513_not_implies_Equation4522 : ∃ (G: Type) (_: Magma G), Equation4513 G ∧ ¬ Equation4522 G := by
   let hG : Magma Nat := {
     op := fun x y => if x = 0 then (if y ≤ 2 then 1 else 2) else x
   }