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

The magma definition

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

Equations

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

The facts

theorem «Facts from FinitePoly [[1,2,0,3],[3,0,2,1],[2,1,3,0],[0,3,1,2]]» : ∃ (G : Type) (x : Magma G), Equation53 G ∧ Equation273 G ∧ Equation281 G ∧ Equation1117 G ∧ Equation1152 G ∧ Equation1155 G ∧ Equation2538 G ∧ Equation4369 G ∧ ¬Equation99 G ∧ ¬Equation203 G ∧ ¬Equation411 G ∧ ¬Equation614 G ∧ ¬Equation817 G ∧ ¬Equation1028 G ∧ ¬Equation1035 G ∧ ¬Equation1039 G ∧ ¬Equation1045 G ∧ ¬Equation1223 G ∧ ¬Equation1426 G ∧ ¬Equation1629 G ∧ ¬Equation1832 G ∧ ¬Equation2035 G ∧ ¬Equation2238 G ∧ ¬Equation2443 G ∧ ¬Equation2449 G ∧ ¬Equation2466 G ∧ ¬Equation2506 G ∧ ¬Equation2644 G ∧ ¬Equation2847 G ∧ ¬Equation3050 G ∧ ¬Equation3253 G ∧ ¬Equation3456 G ∧ ¬Equation3659 G ∧ ¬Equation3862 G ∧ ¬Equation4065 G ∧ ¬Equation4270 G ∧ ¬Equation4275 G ∧ ¬Equation4283 G ∧ ¬Equation4320 G ∧ ¬Equation4380 G ∧ ¬Equation4585 G ∧ ¬Equation4590 G ∧ ¬Equation4635 G