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

The magma definition

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

Equations

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

The facts

theorem «Facts from FinitePoly [[3,4,1,2,0], [2,0,4,1,3], [0,1,2,3,4], [1,3,0,4,2], [4,2,3,0,1]]» : ∃ (G : Type) (x : Magma G), Equation209 G ∧ Equation219 G ∧ Equation231 G ∧ Equation620 G ∧ Equation633 G ∧ Equation670 G ∧ Equation704 G ∧ Equation716 G ∧ Equation826 G ∧ Equation833 G ∧ Equation873 G ∧ Equation880 G ∧ Equation919 G ∧ Equation1435 G ∧ Equation1445 G ∧ Equation1452 G ∧ Equation1479 G ∧ Equation1528 G ∧ Equation3091 G ∧ Equation3140 G ∧ Equation3201 G ∧ Equation4276 G ∧ Equation4362 G ∧ Equation4608 G ∧ Equation4647 G ∧ ¬Equation47 G ∧ ¬Equation99 G ∧ ¬Equation151 G ∧ ¬Equation206 G ∧ ¬Equation211 G ∧ ¬Equation212 G ∧ ¬Equation221 G ∧ ¬Equation222 G ∧ ¬Equation228 G ∧ ¬Equation229 G ∧ ¬Equation255 G ∧ ¬Equation411 G ∧ ¬Equation615 G ∧ ¬Equation616 G ∧ ¬Equation617 G ∧ ¬Equation619 G ∧ ¬Equation622 G ∧ ¬Equation623 G ∧ ¬Equation629 G ∧ ¬Equation630 G ∧ ¬Equation632 G ∧ ¬Equation639 G ∧ ¬Equation640 G ∧ ¬Equation642 G ∧ ⋯