Equational Theories

Reference: Equational Theories project site

class Magma (α : Type) : Type

• op : α → α → α

def «term_◇_» : Lean.TrailingParserDescr

Equations

• «term_◇_» = Lean.ParserDescr.trailingNode `«term_◇_» 65 66 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◇ ") (Lean.ParserDescr.cat `term 66))

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

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

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

theorem 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 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 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.