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

The magma definition

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

Equations

• One or more equations did not get rendered due to their size.

The facts

theorem «Facts from FinitePoly [[0,2,3,4,1,6,7,8,5],[5,1,7,8,2,3,4,6,0],[8,3,2,6,7,1,5,0,4],[7,6,4,3,5,8,0,1,2],[6,8,5,1,4,0,2,3,7],[3,4,0,7,8,5,1,2,6],[2,0,8,5,3,7,6,4,1],[1,5,6,2,0,4,8,7,3],[4,7,1,0,6,2,3,5,8]]» : ∃ (G : Type) (x : Magma G), Equation474 G ∧ Equation3113 G ∧ ¬Equation419 G ∧ ¬Equation429 G ∧ ¬Equation436 G ∧ ¬Equation437 G ∧ ¬Equation464 G ∧ ¬Equation466 G ∧ ¬Equation473 G ∧ ¬Equation504 G ∧ ¬Equation826 G ∧ ¬Equation872 G ∧ ¬Equation917 G ∧ ¬Equation1039 G ∧ ¬Equation1045 G ∧ ¬Equation1075 G ∧ ¬Equation1086 G ∧ ¬Equation1122 G ∧ ¬Equation1632 G ∧ ¬Equation1654 G ∧ ¬Equation1655 G ∧ ¬Equation1658 G ∧ ¬Equation1691 G ∧ ¬Equation1722 G ∧ ¬Equation1731 G ∧ ¬Equation1838 G ∧ ¬Equation1840 G ∧ ¬Equation1861 G ∧ ¬Equation1897 G ∧ ¬Equation1921 G ∧ ¬Equation1925 G ∧ ¬Equation2449 G ∧ ¬Equation2457 G ∧ ¬Equation2533 G ∧ ¬Equation2541 G ∧ ¬Equation2660 G ∧ ¬Equation2710 G ∧ ¬Equation2743 G ∧ ¬Equation3056 G ∧ ¬Equation3058 G ∧ ¬Equation3066 G ∧ ¬Equation3068 G ∧ ¬Equation3075 G ∧ ¬Equation3103 G ∧ ¬Equation3115 G ∧ ¬Equation3143 G ∧ ¬Equation3261 G ∧ ¬Equation3278 G ∧ ¬Equation3306 G ∧ ⋯