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

The magma definition

def «FinitePoly [[0,2,3,4,5,6,1],[6,1,0,5,3,2,4],[1,5,2,0,6,4,3],[2,4,6,3,0,1,5],[3,6,5,1,4,0,2],[4,3,1,6,2,5,0],[5,0,4,2,1,3,6]]» : 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,4,5,6,1],[6,1,0,5,3,2,4],[1,5,2,0,6,4,3],[2,4,6,3,0,1,5],[3,6,5,1,4,0,2],[4,3,1,6,2,5,0],[5,0,4,2,1,3,6]]» : ∃ (G : Type) (x : Magma G), Equation713 G ∧ Equation2450 G ∧ ¬Equation55 G ∧ ¬Equation65 G ∧ ¬Equation619 G ∧ ¬Equation825 G ∧ ¬Equation832 G ∧ ¬Equation872 G ∧ ¬Equation879 G ∧ ¬Equation1434 G ∧ ¬Equation1451 G ∧ ¬Equation1478 G ∧ ¬Equation1491 G ∧ ¬Equation1518 G ∧ ¬Equation1655 G ∧ ¬Equation1840 G ∧ ¬Equation1851 G ∧ ¬Equation2254 G ∧ ¬Equation2263 G ∧ ¬Equation2467 G ∧ ¬Equation3056 G ∧ ¬Equation3068 G ∧ ¬Equation3079 G ∧ ¬Equation3261 G ∧ ¬Equation3306 G ∧ ¬Equation3867 G ∧ ¬Equation3877 G ∧ ¬Equation3887 G ∧ ¬Equation3925 G ∧ ¬Equation3952 G ∧ ¬Equation4070 G ∧ ¬Equation4071 G ∧ ¬Equation4080 G ∧ ¬Equation4090 G ∧ ¬Equation4128 G ∧ ¬Equation4130 G ∧ ¬Equation4155 G ∧ ¬Equation4165 G ∧ ¬Equation4275 G ∧ ¬Equation4320 G ∧ ¬Equation4606 G ∧ ¬Equation4666 G