This file is generated from the following refutation as produced by random generation of polynomials: '(0 * x2 + 2 * y2 + 1 * x + 0 * y + 0 * x * y) % 3' (0, 254, 263, 816, 845, 1019, 1048, 3252, 3318, 4597, 4672)

The magma definition

def «FinitePoly 2 * y² + x % 3» : Magma (Fin 3)

Equations

• «FinitePoly 2 * y² + x % 3» = { op := MemoFinOp.opOfTable 10257 }

The facts

theorem «Facts from FinitePoly 2 * y² + x % 3» : ∃ (G : Type) (x : Magma G) (_ : Finite G), Equation264 G ∧ Equation846 G ∧ Equation1049 G ∧ Equation3319 G ∧ ¬Equation47 G ∧ ¬Equation99 G ∧ ¬Equation151 G ∧ ¬Equation203 G ∧ ¬Equation258 G ∧ ¬Equation261 G ∧ ¬Equation263 G ∧ ¬Equation271 G ∧ ¬Equation273 G ∧ ¬Equation274 G ∧ ¬Equation280 G ∧ ¬Equation281 G ∧ ¬Equation283 G ∧ ¬Equation307 G ∧ ¬Equation411 G ∧ ¬Equation614 G ∧ ¬Equation818 G ∧ ¬Equation819 G ∧ ¬Equation820 G ∧ ¬Equation822 G ∧ ¬Equation823 G ∧ ¬Equation825 G ∧ ¬Equation826 G ∧ ¬Equation832 G ∧ ¬Equation833 G ∧ ¬Equation835 G ∧ ¬Equation836 G ∧ ¬Equation842 G ∧ ¬Equation843 G ∧ ¬Equation845 G ∧ ¬Equation869 G ∧ ¬Equation870 G ∧ ¬Equation872 G ∧ ¬Equation873 G ∧ ¬Equation879 G ∧ ¬Equation880 G ∧ ¬Equation882 G ∧ ¬Equation883 G ∧ ¬Equation906 G ∧ ¬Equation907 G ∧ ¬Equation909 G ∧ ¬Equation910 G ∧ ¬Equation916 G ∧ ¬Equation917 G ∧ ⋯