This file is generated from the following refutation as produced by random generation of polynomials: '(1 * x2 + 1 * y2 + 0 * x + 1 * y + 2 * x * y) % 3' (0, 202, 204, 2237, 2239, 2242, 2245, 2248, 2440, 2458, 4064, 4127, 4267, 4281)

The magma definition

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

Equations

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

The facts

theorem «Facts from FinitePoly x² + y² + y + 2 * x * y % 3» : ∃ (G : Type) (x : Magma G) (_ : Finite G), Equation205 G ∧ Equation2459 G ∧ Equation4128 G ∧ Equation4268 G ∧ ¬Equation47 G ∧ ¬Equation99 G ∧ ¬Equation151 G ∧ ¬Equation206 G ∧ ¬Equation209 G ∧ ¬Equation211 G ∧ ¬Equation212 G ∧ ¬Equation219 G ∧ ¬Equation221 G ∧ ¬Equation222 G ∧ ¬Equation228 G ∧ ¬Equation229 G ∧ ¬Equation231 G ∧ ¬Equation255 G ∧ ¬Equation359 G ∧ ¬Equation411 G ∧ ¬Equation614 G ∧ ¬Equation817 G ∧ ¬Equation1020 G ∧ ¬Equation1223 G ∧ ¬Equation1426 G ∧ ¬Equation1629 G ∧ ¬Equation1832 G ∧ ¬Equation2035 G ∧ ¬Equation2239 G ∧ ¬Equation2241 G ∧ ¬Equation2244 G ∧ ¬Equation2247 G ∧ ¬Equation2253 G ∧ ¬Equation2254 G ∧ ¬Equation2256 G ∧ ¬Equation2257 G ∧ ¬Equation2263 G ∧ ¬Equation2264 G ∧ ¬Equation2266 G ∧ ¬Equation2267 G ∧ ¬Equation2290 G ∧ ¬Equation2291 G ∧ ¬Equation2293 G ∧ ¬Equation2294 G ∧ ¬Equation2300 G ∧ ¬Equation2301 G ∧ ¬Equation2303 G ∧ ¬Equation2304 G ∧ ⋯