Differences

This shows you the differences between two versions of the page.

equations [2017/10/01 19:59]
jipsen
equations [2017/10/02 10:57] (current)
jipsen
Line 46: Line 46:
|42  |entropic:  | $(x*y)*(z*w) = (x*z)*(y*w)$  ||| |42  |entropic:  | $(x*y)*(z*w) = (x*z)*(y*w)$  |||
|43  |paramedial:  | $(x*y)*(z*w) = (w*y)*(z*x)$  ||| |43  |paramedial:  | $(x*y)*(z*w) = (w*y)*(z*x)$  |||
-|44  |Moufang1:  | $((x*y)*x)*z = x*(y*(x*z)$  | Moufang2:  | $((x*y)*z)*y = x*(y*(z*y)$  |+|44  |Moufang1:  | $((x*y)*x)*z = x*(y*(x*z))$  | Moufang2:  | $((x*y)*z)*y = x*(y*(z*y))$  |
|45  |Moufang3:  | $(x*y)*(z*x) = (x*(y*z))*x$  | Moufang4:  | $(x*y)*(z*x) = x*((y*z)*x)$  | |45  |Moufang3:  | $(x*y)*(z*x) = (x*(y*z))*x$  | Moufang4:  | $(x*y)*(z*x) = x*((y*z)*x)$  |
 +Here are the identities in the syntax of the Lean Theorem Prover
 +
 +<code>
 +section identities
 +
 +variables {α: Type u} {β: Type v}
 +variables f g: α → α → α
 +variables h k: α → α
 +variable  c: α
 +local notation a⬝b  := f a b
 +local notation a+b := g a b
 +local notation a⁻¹ := h a
 +local notation 1   := c
 +local notation 0   := c
 +
 +def involutive              := ∀x,     h(h x) = x
 +def inverse_operations      := ∀x,     h(k x) = x
 +def left_absorption         := ∀x,     h(k x) = k x
 +def right_absorption        := ∀x,     h(k x) = h x
 +def unary_idempotent        := ∀x,     h(h x) = h x
 +def idempotent              := ∀x,     x⬝x = x
 +def left_identity           := ∀x,     1⬝x = x
 +def right_identity          := ∀x,     x⬝1 = x
 +def left_zero               := ∀x,     0⬝x = 0
 +def right_zero              := ∀x,     x⬝0 = 0
 +def left_inverse            := ∀x,     x⁻¹⬝x = 1
 +def right_inverse           := ∀x,     x⬝x⁻¹ = 1
 +def left_const_mult         := ∀x,     c⬝x = h x
 +def right_const_mult        := ∀x,     x⬝c = h x
 +def square_constant         := ∀x,     x⬝x = c
 +def square_unary            := ∀x,     x⬝x = h x
 +def left_unary_identity     := ∀x,     (h x)⬝x = x
 +def right_unary_identity    := ∀x,     x⬝(h x) = x
 +def left_unary_const_mult   := ∀x,     h(c⬝x) = c⬝(h x)
 +def right_unary_const_mult  := ∀x,     h(x⬝c) = (h x)⬝c
 +def commutative             := ∀x y,   x⬝y = y⬝x
 +def left_unary_projection   := ∀x y,   x⬝y = h x
 +def right_unary_projection  := ∀x y,   x⬝y = h y
 +def left_idempotent         := ∀x y,   x⬝(x⬝y) = x⬝y
 +def right_idempotent        := ∀x y,   (x⬝y)⬝y = x⬝y
 +def left_rectangular        := ∀x y,   (x⬝y)⬝x = x
 +def right_rectangular       := ∀x y,   x⬝(y⬝x) = x
 +def left_absorption1        := ∀x y,   (x⬝y)+y = y
 +def right_absorption1       := ∀x y,   y+(x⬝y) = y
 +def left_absorption2        := ∀x y,   (x⬝y)+x = x
 +def right_absorption2       := ∀x y,   x+(y⬝x) = x
 +def left_subtraction        := ∀x y,   x⬝(x+y) = y
 +def right_subtraction       := ∀x y,   (y+x)⬝x = y
 +def unary_commutative       := ∀x y,   (h x)⬝(h y) = (h y)⬝(h x)
 +def unary_involutive        := ∀x y,   h(x⬝y) = (h y)⬝(h x)
 +def interdistributive       := ∀x y,   h(x⬝y) = (h x)+(h y)
 +def unary_distributive      := ∀x y,   h(x⬝y) = (h x)⬝(h y)
 +def left_twisted            := ∀x y,   (h(x⬝y))⬝x = x⬝(h y)
 +def right_twisted           := ∀x y,   x⬝(h(y⬝x)) = (h y)⬝x
 +def left_locality           := ∀x y,   h((h x)⬝y) = h(x⬝y)
 +def right_locality          := ∀x y,   h(x⬝(h y)) = h(x⬝y)
 +def left_unary_distributive := ∀x y,   h((h x)⬝y) = (h x)⬝(h y)
 +def right_unary_distributive:= ∀x y,   h(x⬝(h y)) = (h x)⬝(h y)
 +def left_absorbtive         := ∀x y,   (h x)⬝(h(x⬝y)) = h(x⬝y)
 +def right_absorbtive        := ∀x y,   (h(x⬝y))⬝(h y) = h(x⬝y)
 +def flexible                := ∀x y,   (x⬝y)⬝x = x⬝(y⬝x)
 +def associative             := ∀x y z, x⬝(y⬝z) = (x⬝y)⬝z
 +def left_commutative        := ∀x y z, x⬝(y⬝z) = y⬝(x⬝z)
 +def right_commutative       := ∀x y z, (x⬝y)⬝z = (x⬝z)⬝y
 +def interassociative1       := ∀x y z, x⬝(y+z) = (x⬝y)+z
 +def interassociative2       := ∀x y z, x⬝(y+z) = (x+y)⬝z
 +def left_distributive       := ∀x y z, x⬝(y+z) = (x⬝y)+(x⬝z)
 +def right_distributive      := ∀x y z, (x+y)⬝z = (x⬝z)+(y⬝z)
 +def left_self_distributive  := ∀x y z, x⬝(y⬝z) = (x⬝y)⬝(x⬝z)
 +def right_self_distributive := ∀x y z, (x⬝y)⬝z = (x⬝z)⬝(y⬝z)
 +def Moufang1                := ∀x y z, ((x⬝y)⬝x)⬝z = x⬝(y⬝(x⬝z))
 +def Moufang2                := ∀x y z, ((x⬝y)⬝z)⬝y = x⬝(y⬝(z⬝y))
 +def Moufang3                := ∀x y z, (x⬝y)⬝(z⬝x) = (x⬝(y⬝z))⬝x
 +def Moufang4                := ∀x y z, (x⬝y)⬝(z⬝x) = x⬝((y⬝z)⬝x)
 +def entropic                := ∀x y z w, (x⬝y)⬝(z⬝w) = (x⬝z)⬝(y⬝w)
 +def paramedial              := ∀x y z w, (x⬝y)⬝(z⬝w) = (w⬝y)⬝(z⬝x)
 +
 +
 +end identities
 +</code>