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

The magma definition

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

Equations

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

The facts

theorem «Facts from All4x4Tables [[1,2,4,0,6,5,3],[4,3,1,5,2,0,6],[0,6,5,1,3,4,2],[5,0,6,2,4,3,1],[3,4,2,6,0,1,5],[2,1,3,4,5,6,0],[6,5,0,3,1,2,4]]» : ∃ (G : Type) (x : Magma G) (_ : Finite G), Equation880 G ∧ ¬Equation47 G ∧ ¬Equation99 G ∧ ¬Equation151 G ∧ ¬Equation221 G ∧ ¬Equation255 G ∧ ¬Equation411 G ∧ ¬Equation614 G ∧ ¬Equation819 G ∧ ¬Equation826 G ∧ ¬Equation832 G ∧ ¬Equation833 G ∧ ¬Equation835 G ∧ ¬Equation836 G ∧ ¬Equation842 G ∧ ¬Equation843 G ∧ ¬Equation845 G ∧ ¬Equation846 G ∧ ¬Equation870 G ∧ ¬Equation872 G ∧ ¬Equation879 G ∧ ¬Equation882 G ∧ ¬Equation883 G ∧ ¬Equation906 G ∧ ¬Equation907 G ∧ ¬Equation917 G ∧ ¬Equation1020 G ∧ ¬Equation1238 G ∧ ¬Equation1239 G ∧ ¬Equation1242 G ∧ ¬Equation1248 G ∧ ¬Equation1249 G ∧ ¬Equation1251 G ∧ ¬Equation1252 G ∧ ¬Equation1276 G ∧ ¬Equation1278 G ∧ ¬Equation1279 G ∧ ¬Equation1285 G ∧ ¬Equation1286 G ∧ ¬Equation1288 G ∧ ¬Equation1315 G ∧ ¬Equation1322 G ∧ ¬Equation1426 G ∧ ¬Equation1629 G ∧ ¬Equation1832 G ∧ ¬Equation2035 G ∧ ¬Equation2238 G ∧ ¬Equation2441 G ∧ ⋯