Equational Theories

Reference: Equational Theories project site

class EquationalTheories_677_255.Magma (α : Type) : Type

• op : α → α → α

def EquationalTheories_677_255.«term_◇_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev EquationalTheories_677_255.Equation255 (G : Type) [Magma G] : Prop

Equations

• EquationalTheories_677_255.Equation255 G = ∀ (x : G), x = ((x ◇ x) ◇ x) ◇ x

@[reducible, inline]

abbrev EquationalTheories_677_255.Equation677 (G : Type) [Magma G] : Prop

Equations

• EquationalTheories_677_255.Equation677 G = ∀ (x y : G), x = y ◇ (x ◇ ((y ◇ x) ◇ y))

theorem EquationalTheories_677_255.Equation255_not_implies_Equation677 : ∃ (G : Type) (x : Magma G), Equation255 G ∧ ¬Equation677 G

theorem EquationalTheories_677_255.Equation677_not_implies_Equation255 : ∃ (G : Type) (x : Magma G), Equation677 G ∧ ¬Equation255 G

theorem EquationalTheories_677_255.Finite.Equation255_not_implies_Equation677 : ∃ (G : Type) (x : Magma G), Finite G ∧ Equation255 G ∧ ¬Equation677 G

Note that this is a stronger form of Equation255_not_implies_Equation677.

theorem EquationalTheories_677_255.Finite.Equation677_not_implies_Equation255 : ∃ (G : Type) (x : Magma G), Finite G ∧ Equation677 G ∧ ¬Equation255 G

The negation of Finite.Equation677_implies_Equation255.

Probably this is true. It would be a stronger form of Equation677_not_implies_Equation255.

Discussion thread here: https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/FINITE.3A.20677.20-.3E.20255

theorem EquationalTheories_677_255.Finite.Equation677_implies_Equation255 (G : Type) [Magma G] [Finite G] (h : Equation677 G) : Equation255 G

The negation of Finite.Equation677_not_implies_Equation255.

Probably this is false.