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

The magma definition

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

Equations

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

The facts

theorem «Facts from All4x4Tables [[1,2,3,4,5,0,6],[5,4,0,3,6,1,2],[4,1,6,5,3,2,0],[0,6,4,2,1,3,5],[3,5,2,6,0,4,1],[6,3,1,0,2,5,4],[2,0,5,1,4,6,3]]» : ∃ (G : Type) (x : Magma G) (_ : Finite G), Equation2328 G ∧ ¬Equation47 G ∧ ¬Equation105 G ∧ ¬Equation107 G ∧ ¬Equation151 G ∧ ¬Equation203 G ∧ ¬Equation255 G ∧ ¬Equation411 G ∧ ¬Equation614 G ∧ ¬Equation817 G ∧ ¬Equation1020 G ∧ ¬Equation1223 G ∧ ¬Equation1427 G ∧ ¬Equation1428 G ∧ ¬Equation1429 G ∧ ¬Equation1431 G ∧ ¬Equation1434 G ∧ ¬Equation1435 G ∧ ¬Equation1441 G ∧ ¬Equation1445 G ∧ ¬Equation1454 G ∧ ¬Equation1478 G ∧ ¬Equation1482 G ∧ ¬Equation1488 G ∧ ¬Equation1515 G ∧ ¬Equation1516 G ∧ ¬Equation1519 G ∧ ¬Equation1629 G ∧ ¬Equation1832 G ∧ ¬Equation2035 G ∧ ¬Equation2240 G ∧ ¬Equation2244 G ∧ ¬Equation2246 G ∧ ¬Equation2247 G ∧ ¬Equation2254 G ∧ ¬Equation2256 G ∧ ¬Equation2257 G ∧ ¬Equation2264 G ∧ ¬Equation2266 G ∧ ¬Equation2291 G ∧ ¬Equation2300 G ∧ ¬Equation2301 G ∧ ¬Equation2303 G ∧ ¬Equation2330 G ∧ ¬Equation2340 G ∧ ¬Equation2441 G ∧ ¬Equation2644 G ∧ ¬Equation2847 G ∧ ⋯