This file is generated from the following operator table: [[1,2,3,4,5,0],[0,5,4,3,2,1],[5,4,1,0,3,2],[4,1,2,5,0,3],[3,0,5,2,1,4],[2,3,0,1,4,5]]
The magma definition
def
«FinitePoly [[1,2,3,4,5,0],[0,5,4,3,2,1],[5,4,1,0,3,2],[4,1,2,5,0,3],[3,0,5,2,1,4],[2,3,0,1,4,5]]» :
Equations
- One or more equations did not get rendered due to their size.
Instances For
The facts
theorem
«Facts from FinitePoly [[1,2,3,4,5,0],[0,5,4,3,2,1],[5,4,1,0,3,2],[4,1,2,5,0,3],[3,0,5,2,1,4],[2,3,0,1,4,5]]» :
∃ (G : Type) (x : Magma G),
Equation917 G ∧ Equation1729 G ∧ ¬Equation411 G ∧ ¬Equation614 G ∧ ¬Equation1832 G ∧ ¬Equation3050 G