Equation 63 to Equation 3167

The constant law: all products are constant. It is self-dual.

DefinitionEquation 63#

Equation 63 is the law \(0 \simeq 1 \diamond (0 \diamond (0 \diamond 1))\) (or the equation \(x = y \diamond (x \diamond (x \diamond y))\)).

Lean

Formalized as Equation63.

Sources

• Equational Theories blueprint: chapter/equations.tex, line 124

LeanEquation63

Uses 1

Statement usesMagma

The “Dupont” law, studied further in The Dupont equation.

DefinitionEquation 65#

Equation 65 is the law \(0 \simeq 1 \diamond (0 \diamond (1 \diamond 0))\) (or the equation \(x = y \diamond (x \diamond (y \diamond x))\)).

Lean

Formalized as Equation65.

Sources

• Equational Theories blueprint: chapter/equations.tex, line 130

LeanEquation65

Uses 1

Statement usesMagma

The “Asterix” law, studied further in The Asterix equation.

DefinitionEquation 168#

Equation 168 is the law \(0 \simeq (1 \diamond 0) \diamond (0 \diamond 2)\) (or the equation \(x = (y \diamond x) \diamond (x \diamond z)\)).

Lean

Formalized as Equation168.

Sources

• Equational Theories blueprint: chapter/equations.tex, line 136

LeanEquation168

Uses 1

Statement usesMagma

The law of a central groupoid. It is self-dual.

DefinitionEquation 206#

Equation 206 is the law \(0 \simeq (0 \diamond (0 \diamond 1)) \diamond 1\) (or the equation \(x = (x \diamond (x \diamond y)) \diamond y\)).

Lean

Formalized as Equation206.

Sources

• Equational Theories blueprint: chapter/equations.tex, line 142

LeanEquation206

Uses 1 · Used by 1

Statement usesMagma

Used by1648 does not imply 206

Our project located this law as one member of an “Austin pair”; see Finite implications and infinite models. The infinite counterexample is constructed using the infinite 3-regular tree.

DefinitionEquation 381#

Equation 381 is the law \(0 \diamond 1 \simeq (0 \diamond 2) \diamond 1\) (or the equation \(x \diamond y = (x \diamond z) \diamond y\)).

Lean

Formalized as Equation381.

Sources

• Equational Theories blueprint: chapter/equations.tex, line 148

LeanEquation381

Uses 1 · Used by 1

Statement usesMagma

Used by3744 implies 3722, 381

Appears in Putnam 1978, Problem A4, part (b).

DefinitionEquation 387#

Equation 387 is the law \(0 \diamond 1 \simeq (1 \diamond 1) \diamond 0\) (or the equation \(x \diamond y = (y \diamond y) \diamond x\)).

Lean

Formalized as Equation387.

Sources

• Equational Theories blueprint: chapter/equations.tex, line 154

LeanEquation387

Uses 1 · Used by 1

Statement usesMagma

Used by387 implies 43

Introduced in MathOverflow. See 387 implies 43

DefinitionEquation 477#

Equation 477 is the law \(0 \simeq 1 \diamond (0 \diamond (1 \diamond (1 \diamond 1)))\) (or the equation \(x = y \diamond (x \diamond (y \diamond (y \diamond y)))\)).

Lean

Formalized as Equation477.

Sources

• Equational Theories blueprint: chapter/equations.tex, line 160

LeanEquation477

Uses 1

Statement usesMagma

An example of a confluent law; see 477 confluent.

DefinitionEquation 854#

Equation 854 is the law \(0 = 0 \diamond ((1 \diamond 2) \diamond (0 \diamond 2))\) (or the equation \(x = x \diamond ((y \diamond z) \diamond (x \diamond z))\)).

Lean

Formalized as Equation953.

Sources

• Equational Theories blueprint: chapter/equations.tex, line 166

LeanEquation953

Uses 1

Statement usesMagma

Studied in Equation 854

DefinitionEquation 953#

Equation 953 is the law \(0 = 1 \diamond ((2 \diamond 0) \diamond (2 \diamond 2))\) (or the equation \(x = y \diamond ((z \diamond x) \diamond (z \diamond z))\)).

Lean

Formalized as Equation953.

Sources

• Equational Theories blueprint: chapter/equations.tex, line 173

LeanEquation953

Uses 1 · Used by 1

Statement usesMagma

Used by953 is equivalent to 2

An example of a trivial law; see 953 is equivalent to 2.

DefinitionEquation 1485#

Equation 1485 is the law \(0 \simeq (1 \diamond 0) \diamond (0 \diamond (2 \diamond 1))\) (or the equation \(x = (y \diamond x) \diamond (x \diamond (z \diamond y))\)).

Lean

Formalized as Equation1491.

Sources

• Equational Theories blueprint: chapter/equations.tex, line 179

LeanEquation1491

Uses 1 · Used by 5

Statement usesMagma

Used by1485 equivalent to 2162 · 1485 does not imply 1483 · Claim 4 · Equivalent characterization of graph · Completion property

The weak central groupoid law, implied by the central groupoid law E168. Studied in Weak central groupoids.

DefinitionEquation 1491#

Equation 1491 is the law \(0 \simeq (1 \diamond 0) \diamond (1 \diamond (1 \diamond 0))\) (or the equation \(x = (y \diamond x) \diamond (y \diamond (y \diamond x))\)).

Lean

Formalized as Equation1491.

Sources

• Equational Theories blueprint: chapter/equations.tex, line 185

LeanEquation1491

Uses 1

Statement usesMagma

The “Obelix” law, studied further in The Asterix equation.

DefinitionEquation 1571#

Equation 1571 is the law \(0 \simeq (1 \diamond 2) \diamond (1 \diamond (0 \diamond 2))\) (or the equation \(x = (y \diamond z) \diamond (y \diamond (x \diamond z))\)).

Lean

Formalized as Equation1571.

Sources

• Equational Theories blueprint: chapter/equations.tex, line 191

LeanEquation1571

Uses 1 · Used by 1

Statement usesMagma

Used byConsequences of 1571

Introduced in (Mendelsohn and Padmanabhan 1975). As shown in Consequences of 1571, this law characterizes abelian groups of exponent two.

DefinitionEquation 1648#

Equation 1648 is the law \(0 \simeq (0 \diamond 1) \diamond ((0 \diamond 1) \diamond 1)\) (or the equation \(x = (x \diamond y) \diamond ((x \diamond y) \diamond y)\)).

Lean

Formalized as Equation1648.

Sources

• Equational Theories blueprint: chapter/equations.tex, line 197

LeanEquation1648

Uses 1 · Used by 1

Statement usesMagma

Used by1648 does not imply 206

The golden ratio is a coefficient of the linearization of this law.

DefinitionEquation 1657#

Equation 1657 is the law \(0 \simeq (0 \diamond 1) \diamond ((1 \diamond 1) \diamond 0)\) (or the equation \(x = (x \diamond y) \diamond ((y \diamond y) \diamond x)\)).

Lean

Formalized as Equation1657.

Sources

• Equational Theories blueprint: chapter/equations.tex, line 203

LeanEquation1657

Uses 1

Statement usesMagma

DefinitionEquation 1659#

Equation 1659 is the law \(0 \simeq (0 \diamond 1) \diamond ((1 \diamond 1) \diamond 2)\) (or the equation \(x = (x \diamond y) \diamond ((y \diamond y) \diamond z)\)).

Lean

Formalized as Equation1659.

Sources

• Equational Theories blueprint: chapter/equations.tex, line 207

LeanEquation1659

Uses 1 · Used by 1

Statement usesMagma

Used by1659 does not imply 4315

DefinitionEquation 1661#

Equation 1661 is the law \(0 \simeq (0 \diamond 1) \diamond ((1 \diamond 2) \diamond 1)\) (or the equation \(x = (x \diamond y) \diamond ((y \diamond z) \diamond y)\)).

Lean

Formalized as Equation1661.

Sources

• Equational Theories blueprint: chapter/equations.tex, line 211

LeanEquation1661

Uses 1

Statement usesMagma

These two laws admit infinite models on the natural numbers arising from the modified base model construction. See A survey of examples.

DefinitionEquation 1689#

Equation 1689 is the law \(0 \simeq (1 \diamond 0) \diamond ((0 \diamond 2) \diamond 2)\) (or the equation \(x = (y \diamond x) \diamond ((x \diamond z) \diamond z)\)).

Lean

Formalized as Equation1689.

Sources

• Equational Theories blueprint: chapter/equations.tex, line 217

LeanEquation1689

Uses 1 · Used by 1

Statement usesMagma

Used by1689 is equivalent to 2

Mentioned in (Kisielewicz 1997). See 1689 is equivalent to 2.

DefinitionEquation 1701#

Equation 1701 is the law \(0 \simeq (1 \diamond x) \diamond ((2 \diamond 0) \diamond 0)\) (or the equation \(x = (y \diamond x) \diamond ((z \diamond x) \diamond x)\)).

Lean

Formalized as Equation1701.

Sources

• Equational Theories blueprint: chapter/equations.tex, line 223

LeanEquation1701

Uses 1

Statement usesMagma

This law admits infinite models on the natural numbers arising from the modified base model construction. See A survey of examples.

DefinitionEquation 2662#

Equation 2662 is the law \(0 \simeq ((0 \diamond 1) \diamond (0 \diamond 1)) \diamond 0\) (or the equation \(x = ((x \diamond y) \diamond (x \diamond y)) \diamond x\)).

Lean

Formalized as Equation2662.

Sources

• Equational Theories blueprint: chapter/equations.tex, line 229

LeanEquation2662

Uses 1 · Used by 1

Statement usesMagma

Used byConsequences of 1571

Appears in (Mendelsohn and Padmanabhan 1975).

DefinitionEquation 3167#

Equation 3167 is the law \(0 \simeq (((1 \diamond 1) \diamond 2) \diamond 2) \diamond 0\) (or the equation \(x = (((y \diamond y) \diamond z) \diamond z) \diamond x\)).

Lean

Formalized as Equation3167.

Sources

• Equational Theories blueprint: chapter/equations.tex, line 235

LeanEquation3167

Uses 1

Statement usesMagma

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.