This file is generated from the following operator table: [[0,0,0],[1,0,2],[2,0,2]]

The magma definition

def «All4x4Tables [[0,0,0],[1,0,2],[2,0,2]]» : Magma (Fin 3)

Equations

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

The facts

theorem «Facts from All4x4Tables [[0,0,0],[1,0,2],[2,0,2]]» : ∃ (G : Type) (x : Magma G) (_ : Finite G), Equation841 G ∧ ¬Equation108 G ∧ ¬Equation414 G ∧ ¬Equation427 G ∧ ¬Equation430 G ∧ ¬Equation436 G ∧ ¬Equation437 G ∧ ¬Equation439 G ∧ ¬Equation440 G ∧ ¬Equation823 G ∧ ¬Equation842 G ∧ ¬Equation843 G ∧ ¬Equation845 G ∧ ¬Equation846 G ∧ ¬Equation1023 G ∧ ¬Equation1036 G ∧ ¬Equation1039 G ∧ ¬Equation1046 G ∧ ¬Equation1049 G ∧ ¬Equation1252 G ∧ ¬Equation1851 G ∧ ¬Equation1857 G ∧ ¬Equation1860 G ∧ ¬Equation1861 G ∧ ¬Equation3256 G ∧ ¬Equation3278 G ∧ ¬Equation3279 G ∧ ¬Equation3306 G ∧ ¬Equation3315 G ∧ ¬Equation3318 G ∧ ¬Equation3663 G ∧ ¬Equation3665 G ∧ ¬Equation3677 G ∧ ¬Equation3684 G ∧ ¬Equation3685 G ∧ ¬Equation3687 G ∧ ¬Equation3729 G ∧ ¬Equation3865 G ∧ ¬Equation3873 G ∧ ¬Equation3878 G ∧ ¬Equation3881 G ∧ ¬Equation3887 G ∧ ¬Equation3888 G ∧ ¬Equation3943 G ∧ ¬Equation4066 G ∧ ¬Equation4067 G ∧ ¬Equation4068 G ∧ ¬Equation4070 G ∧ ⋯