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

The magma definition

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

Equations

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

The facts

theorem «Facts from FinitePoly [[0,2,3,4,1],[2,1,4,0,3],[3,4,2,1,0],[4,0,1,3,2],[1,3,0,2,4]]» : ∃ (G : Type) (x : Magma G), Equation63 G ∧ Equation65 G ∧ Equation124 G ∧ Equation206 G ∧ Equation271 G ∧ Equation1489 G ∧ Equation1491 G ∧ Equation1516 G ∧ Equation1518 G ∧ Equation1648 G ∧ Equation1692 G ∧ Equation1895 G ∧ Equation1924 G ∧ Equation2091 G ∧ Equation3269 G ∧ Equation4081 G ∧ ¬Equation50 G ∧ ¬Equation55 G ∧ ¬Equation56 G ∧ ¬Equation66 G ∧ ¬Equation73 G ∧ ¬Equation75 G ∧ ¬Equation105 G ∧ ¬Equation107 G ∧ ¬Equation108 G ∧ ¬Equation118 G ∧ ¬Equation127 G ∧ ¬Equation159 G ∧ ¬Equation160 G ∧ ¬Equation167 G ∧ ¬Equation211 G ∧ ¬Equation221 G ∧ ¬Equation229 G ∧ ¬Equation231 G ∧ ¬Equation263 G ∧ ¬Equation264 G ∧ ¬Equation274 G ∧ ¬Equation280 G ∧ ¬Equation283 G ∧ ¬Equation412 G ∧ ¬Equation413 G ∧ ¬Equation414 G ∧ ¬Equation416 G ∧ ¬Equation417 G ∧ ¬Equation419 G ∧ ¬Equation420 G ∧ ¬Equation426 G ∧ ¬Equation430 G ∧ ¬Equation436 G ∧ ⋯