This file is generated from the following operator table: [[5,1,2,0,5,4],[2,0,0,3,1,5],[1,0,0,5,2,3],[4,5,3,1,0,1],[5,2,1,4,5,0],[0,3,5,1,4,1]]
The magma definition
def
«All4x4Tables [[5,1,2,0,5,4],[2,0,0,3,1,5],[1,0,0,5,2,3],[4,5,3,1,0,1],[5,2,1,4,5,0],[0,3,5,1,4,1]]» :
Equations
- One or more equations did not get rendered due to their size.
Instances For
The facts
theorem
«Facts from All4x4Tables [[5,1,2,0,5,4],[2,0,0,3,1,5],[1,0,0,5,2,3],[4,5,3,1,0,1],[5,2,1,4,5,0],[0,3,5,1,4,1]]» :
∃ (G : Type) (x : Magma G) (_ : Finite G),
Equation3342 G ∧ Equation3964 G ∧ ¬Equation3306 G ∧ ¬Equation3308 G ∧ ¬Equation3315 G ∧ ¬Equation3319 G ∧ ¬Equation3346 G ∧ ¬Equation3353 G ∧ ¬Equation3509 G ∧ ¬Equation3511 G ∧ ¬Equation3518 G ∧ ¬Equation3545 G ∧ ¬Equation3549 G ∧ ¬Equation3556 G ∧ ¬Equation3558 G ∧ ¬Equation3659 G ∧ ¬Equation3915 G ∧ ¬Equation3917 G ∧ ¬Equation3924 G ∧ ¬Equation3928 G ∧ ¬Equation3951 G ∧ ¬Equation3955 G ∧ ¬Equation3962 G ∧ ¬Equation4120 G ∧ ¬Equation4127 G ∧ ¬Equation4131 G ∧ ¬Equation4158 G ∧ ¬Equation4165 G ∧ ¬Equation4167 G ∧ ¬Equation4283 G ∧ ¬Equation4290 G ∧ ¬Equation4320 G ∧ ¬Equation4380 G ∧ ¬Equation4598 G ∧ ¬Equation4605 G ∧ ¬Equation4635 G