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

The magma definition

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

Equations

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

The facts

theorem «Facts from FinitePoly [[0,0],[1,0]]» : ∃ (G : Type) (x : Magma G), Equation106 G ∧ Equation371 G ∧ Equation1043 G ∧ Equation1271 G ∧ Equation3285 G ∧ Equation3306 G ∧ Equation3321 G ∧ Equation3895 G ∧ Equation3931 G ∧ Equation4101 G ∧ Equation4293 G ∧ Equation4673 G ∧ ¬Equation47 G ∧ ¬Equation151 G ∧ ¬Equation203 G ∧ ¬Equation255 G ∧ ¬Equation307 G ∧ ¬Equation416 G ∧ ¬Equation417 G ∧ ¬Equation419 G ∧ ¬Equation420 G ∧ ¬Equation614 G ∧ ¬Equation825 G ∧ ¬Equation826 G ∧ ¬Equation1026 G ∧ ¬Equation1029 G ∧ ¬Equation1426 G ∧ ¬Equation1629 G ∧ ¬Equation1833 G ∧ ¬Equation1837 G ∧ ¬Equation1838 G ∧ ¬Equation1840 G ∧ ¬Equation1841 G ∧ ¬Equation1848 G ∧ ¬Equation1858 G ∧ ¬Equation2035 G ∧ ¬Equation2238 G ∧ ¬Equation2441 G ∧ ¬Equation2644 G ∧ ¬Equation2847 G ∧ ¬Equation3050 G ∧ ¬Equation3258 G ∧ ¬Equation3259 G ∧ ¬Equation3261 G ∧ ¬Equation3262 G ∧ ¬Equation3268 G ∧ ¬Equation3269 G ∧ ¬Equation3271 G ∧ ¬Equation3272 G ∧ ⋯