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

The magma definition

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

Equations

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

The facts

theorem «Facts from FinitePoly [[1,0,2,3],[2,1,0,3],[0,2,1,3],[0,1,2,3]]» : ∃ (G : Type) (x : Magma G), Equation273 G ∧ Equation882 G ∧ Equation906 G ∧ Equation2506 G ∧ Equation3749 G ∧ ¬Equation47 G ∧ ¬Equation107 G ∧ ¬Equation151 G ∧ ¬Equation211 G ∧ ¬Equation221 G ∧ ¬Equation231 G ∧ ¬Equation280 G ∧ ¬Equation283 G ∧ ¬Equation307 G ∧ ¬Equation413 G ∧ ¬Equation416 G ∧ ¬Equation426 G ∧ ¬Equation429 G ∧ ¬Equation473 G ∧ ¬Equation476 G ∧ ¬Equation503 G ∧ ¬Equation614 G ∧ ¬Equation819 G ∧ ¬Equation825 G ∧ ¬Equation832 G ∧ ¬Equation845 G ∧ ¬Equation872 G ∧ ¬Equation879 G ∧ ¬Equation1022 G ∧ ¬Equation1025 G ∧ ¬Equation1028 G ∧ ¬Equation1035 G ∧ ¬Equation1038 G ∧ ¬Equation1048 G ∧ ¬Equation1082 G ∧ ¬Equation1085 G ∧ ¬Equation1109 G ∧ ¬Equation1112 G ∧ ¬Equation1223 G ∧ ¬Equation1426 G ∧ ¬Equation1631 G ∧ ¬Equation1634 G ∧ ¬Equation1637 G ∧ ¬Equation1644 G ∧ ¬Equation1654 G ∧ ¬Equation1657 G ∧ ¬Equation1681 G ∧ ¬Equation1684 G ∧ ¬Equation1694 G ∧ ⋯