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

The magma definition

def «FinitePoly [[1,3,0,1],[3,3,1,0],[3,0,2,1],[1,0,3,0]]» : Magma (Fin 4)

Equations

• «FinitePoly [[1,3,0,1],[3,3,1,0],[3,0,2,1],[1,0,3,0]]» = { op := MemeFinOp.opOfTable 828579661 }

The facts

theorem «Facts from FinitePoly [[1,3,0,1],[3,3,1,0],[3,0,2,1],[1,0,3,0]]» : ∃ (G : Type) (x : Magma G), Equation3355 G ∧ ¬Equation307 G ∧ ¬Equation359 G ∧ ¬Equation3306 G ∧ ¬Equation3308 G ∧ ¬Equation3309 G ∧ ¬Equation3315 G ∧ ¬Equation3316 G ∧ ¬Equation3318 G ∧ ¬Equation3319 G ∧ ¬Equation3342 G ∧ ¬Equation3343 G ∧ ¬Equation3345 G ∧ ¬Equation3346 G ∧ ¬Equation3352 G ∧ ¬Equation3353 G ∧ ¬Equation3509 G ∧ ¬Equation3511 G ∧ ¬Equation3512 G ∧ ¬Equation3518 G ∧ ¬Equation3519 G ∧ ¬Equation3521 G ∧ ¬Equation3522 G ∧ ¬Equation3545 G ∧ ¬Equation3546 G ∧ ¬Equation3548 G ∧ ¬Equation3549 G ∧ ¬Equation3555 G ∧ ¬Equation3556 G ∧ ¬Equation3558 G ∧ ¬Equation3659 G ∧ ¬Equation3915 G ∧ ¬Equation3917 G ∧ ¬Equation3918 G ∧ ¬Equation3924 G ∧ ¬Equation3925 G ∧ ¬Equation3927 G ∧ ¬Equation3928 G ∧ ¬Equation3951 G ∧ ¬Equation3952 G ∧ ¬Equation3954 G ∧ ¬Equation3955 G ∧ ¬Equation3961 G ∧ ¬Equation3962 G ∧ ¬Equation3964 G ∧ ¬Equation4118 G ∧ ¬Equation4120 G ∧ ¬Equation4121 G ∧ ¬Equation4127 G ∧ ⋯