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

The magma definition

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

Equations

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

The facts

theorem «Facts from FinitePoly [[0,2,3,1,6,4,5],[1,4,5,2,0,3,6],[2,3,6,4,1,5,0],[3,6,1,5,4,0,2],[4,5,0,3,2,6,1],[5,0,2,6,3,1,4],[6,1,4,0,5,2,3]]» : ∃ (G : Type) (x : Magma G), Equation1313 G ∧ Equation1315 G ∧ Equation1322 G ∧ ¬Equation151 G ∧ ¬Equation411 G ∧ ¬Equation1020 G ∧ ¬Equation1228 G ∧ ¬Equation1238 G ∧ ¬Equation1248 G ∧ ¬Equation1278 G ∧ ¬Equation1288 G ∧ ¬Equation2035 G ∧ ¬Equation3659 G ∧ ¬Equation3862 G ∧ ¬Equation4065 G ∧ ¬Equation4275 G ∧ ¬Equation4320 G ∧ ¬Equation4321 G ∧ ¬Equation4380 G ∧ ¬Equation4605 G ∧ ¬Equation4606 G ∧ ¬Equation4635 G ∧ ¬Equation4636 G ∧ ¬Equation4666 G