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

The magma definition

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

Equations

• «FinitePoly [[2,1,0,1],[2,3,1,1],[2,3,0,2],[0,3,0,1]]» = { op := MemeFinOp.opOfTable 1284398662 }

The facts

theorem «Facts from FinitePoly [[2,1,0,1],[2,3,1,1],[2,3,0,2],[0,3,0,1]]» : ∃ (G : Type) (x : Magma G), Equation1687 G ∧ ¬Equation1038 G ∧ ¬Equation1225 G ∧ ¬Equation1238 G ∧ ¬Equation1248 G ∧ ¬Equation1634 G ∧ ¬Equation1644 G ∧ ¬Equation1654 G ∧ ¬Equation1691 G ∧ ¬Equation1837 G ∧ ¬Equation1847 G ∧ ¬Equation1857 G ∧ ¬Equation1884 G ∧ ¬Equation1921 G ∧ ¬Equation3306 G ∧ ¬Equation3309 G ∧ ¬Equation3343 G ∧ ¬Equation3346 G ∧ ¬Equation3353 G ∧ ¬Equation3880 G ∧ ¬Equation4067 G ∧ ¬Equation4080 G ∧ ¬Equation4090 G ∧ ¬Equation4118 G ∧ ¬Equation4128 G ∧ ¬Equation4155 G ∧ ¬Equation4284 G ∧ ¬Equation4291 G ∧ ¬Equation4320 G ∧ ¬Equation4635 G ∧ ¬Equation4666 G