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

The magma definition

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

Equations

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

The facts

theorem «Facts from FinitePoly [[0,1,2,3],[2,3,1,0],[1,2,3,0],[1,3,0,2]]» : ∃ (G : Type) (x : Magma G), Equation420 G ∧ Equation501 G ∧ ¬Equation47 G ∧ ¬Equation99 G ∧ ¬Equation151 G ∧ ¬Equation211 G ∧ ¬Equation221 G ∧ ¬Equation255 G ∧ ¬Equation413 G ∧ ¬Equation416 G ∧ ¬Equation417 G ∧ ¬Equation419 G ∧ ¬Equation426 G ∧ ¬Equation429 G ∧ ¬Equation436 G ∧ ¬Equation437 G ∧ ¬Equation440 G ∧ ¬Equation466 G ∧ ¬Equation477 G ∧ ¬Equation614 G ∧ ¬Equation817 G ∧ ¬Equation1020 G ∧ ¬Equation1223 G ∧ ¬Equation1426 G ∧ ¬Equation1629 G ∧ ¬Equation1832 G ∧ ¬Equation2035 G ∧ ¬Equation2238 G ∧ ¬Equation2441 G ∧ ¬Equation2644 G ∧ ¬Equation2847 G ∧ ¬Equation3050 G ∧ ¬Equation3253 G ∧ ¬Equation3456 G ∧ ¬Equation3659 G ∧ ¬Equation3862 G ∧ ¬Equation4065 G ∧ ¬Equation4268 G ∧ ¬Equation4269 G ∧ ¬Equation4270 G ∧ ¬Equation4273 G ∧ ¬Equation4283 G ∧ ¬Equation4284 G ∧ ¬Equation4290 G ∧ ¬Equation4314 G ∧ ¬Equation4380 G ∧ ¬Equation4583 G ∧ ¬Equation4584 G ∧ ¬Equation4585 G ∧ ¬Equation4588 G ∧ ¬Equation4598 G ∧ ¬Equation4599 G ∧ ¬Equation4605 G ∧ ¬Equation4629 G