This file is generated from the following refutation as produced by random generation of polynomials: '(0 * x2 + 2 * y2 + 1 * x + 1 * y + 2 * x * y) % 4' (0, 22, 25, 410, 416, 428, 439, 451, 463, 472, 503, 512, 545, 561, 816, 824, 832, 845, 860, 871, 878, 909, 916, 948, 961, 1019, 1025, 1037, 1048, 1060, 1072, 1081, 1112, 1121, 1154, 1170, 1628, 1631, 1653, 1657, 1661, 1681, 1683, 1728, 1730, 1789, 1792, 1831, 1837, 1849, 1860, 1872, 1884, 1893, 1924, 1933, 1966, 1982, 2440, 2448, 2456, 2469, 2484, 2495, 2502, 2533, 2540, 2572, 2585, 3049, 3052, 3055, 3057, 3065, 3067, 3074, 3078, 3082, 3090, 3093, 3455, 3458, 3471, 3473, 3517, 3521, 3525, 3555, 3557, 3600, 3606, 4064, 4067, 4070, 4072, 4117, 4119, 4126, 4130, 4134, 4142, 4145, 4272, 4289, 4331, 4368, 4584, 4597, 4655, 4672)

The magma definition

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

Equations

• «FinitePoly 2 * y² + x + y + 2 * x * y % 4» = { op := MemeFinOp.opOfTable 2479241580 }

The facts

theorem «Facts from FinitePoly 2 * y² + x + y + 2 * x * y % 4» : ∃ (G : Type) (x : Magma G), Equation26 G ∧ Equation452 G ∧ Equation546 G ∧ Equation562 G ∧ Equation861 G ∧ Equation949 G ∧ Equation962 G ∧ Equation1061 G ∧ Equation1155 G ∧ Equation1171 G ∧ Equation1790 G ∧ Equation1793 G ∧ Equation1967 G ∧ Equation1983 G ∧ Equation2573 G ∧ Equation2586 G ∧ Equation3601 G ∧ Equation3607 G ∧ Equation4143 G ∧ Equation4273 G ∧ ¬Equation47 G ∧ ¬Equation99 G ∧ ¬Equation151 G ∧ ¬Equation203 G ∧ ¬Equation255 G ∧ ¬Equation359 G ∧ ¬Equation412 G ∧ ¬Equation413 G ∧ ¬Equation414 G ∧ ¬Equation416 G ∧ ¬Equation419 G ∧ ¬Equation420 G ∧ ¬Equation426 G ∧ ¬Equation427 G ∧ ¬Equation430 G ∧ ¬Equation436 G ∧ ¬Equation437 G ∧ ¬Equation439 G ∧ ¬Equation463 G ∧ ¬Equation466 G ∧ ¬Equation467 G ∧ ¬Equation474 G ∧ ¬Equation476 G ∧ ¬Equation477 G ∧ ¬Equation500 G ∧ ¬Equation501 G ∧ ¬Equation503 G ∧ ¬Equation510 G ∧ ¬Equation511 G ∧ ⋯