This file is generated from the following refutation as produced by random generation of polynomials: '(0 * x2 + 2 * y2 + 3 * x + 1 * y + 0 * x * y) % 4' (0, 7, 13, 15, 22, 25, 28, 42, 410, 416, 418, 435, 463, 465, 476, 488, 491, 499, 510, 512, 521, 527, 571, 574, 613, 616, 619, 629, 668, 675, 679, 683, 691, 702, 706, 710, 713, 724, 745, 758, 1019, 1035, 1037, 1044, 1072, 1074, 1081, 1112, 1119, 1121, 1151, 1154, 1164, 1170, 1180, 1183, 1222, 1225, 1230, 1240, 1275, 1284, 1288, 1292, 1303, 1311, 1315, 1319, 1324, 1339, 1357, 1373, 1425, 1431, 1433, 1441, 1443, 1454, 1466, 1469, 1478, 1480, 1491, 1503, 1506, 1518, 1557, 1560, 1628, 1631, 1634, 1646, 1653, 1657, 1661, 1669, 1683, 1690, 1694, 1698, 1706, 1730, 1779, 1792, 1831, 1837, 1839, 1847, 1849, 1860, 1872, 1875, 1893, 1920, 1931, 1933, 1942, 1948, 1976, 1982, 2034, 2050, 2052, 2059, 2087, 2089, 2096, 2127, 2134, 2136, 2166, 2169, 2179, 2185, 2195, 2198, 2237, 2240, 2243, 2255, 2262, 2266, 2270, 2278, 2290, 2326, 2330, 2334, 2337, 2348, 2372, 2398, 2440, 2446, 2448, 2456, 2458, 2469, 2481, 2484, 2493, 2495, 2506, 2518, 2521, 2533, 2572, 2575, 2846, 2849, 2852, 2862, 2901, 2908, 2912, 2916, 2924, 2935, 2939, 2943, 2946, 2957, 2978, 2991, 3049, 3052, 3057, 3065, 3074, 3078, 3082, 3093, 3102, 3111, 3115, 3119, 3130, 3149, 3194, 3210, 3252, 3258, 3260, 3277, 3305, 3307, 3318, 3330, 3333, 3341, 3352, 3354, 3363, 3369, 3413, 3416, 3455, 3458, 3461, 3471, 3510, 3517, 3521, 3525, 3533, 3544, 3548, 3552, 3555, 3566, 3587, 3600, 3861, 3877, 3879, 3886, 3914, 3916, 3923, 3954, 3961, 3963, 3993, 3996, 4006, 4012, 4022, 4025, 4064, 4067, 4072, 4082, 4117, 4126, 4130, 4134, 4145, 4153, 4157, 4161, 4166, 4181, 4199, 4215, 4272, 4274, 4282, 4304, 4306, 4331, 4357, 4379, 4382, 4385, 4397, 4404, 4408, 4412, 4420, 4434, 4441, 4445, 4449, 4457, 4481, 4530, 4543, 4584, 4587, 4634, 4639, 4646, 4655, 4676)

The magma definition

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

Equations

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

The facts

theorem «Facts from FinitePoly 2 * y² + 3 * x + y % 4» : ∃ (G : Type) (x : Magma G) (_ : Finite G), Equation14 G ∧ Equation16 G ∧ Equation26 G ∧ Equation43 G ∧ Equation492 G ∧ Equation522 G ∧ Equation572 G ∧ Equation684 G ∧ Equation692 G ∧ Equation711 G ∧ Equation725 G ∧ Equation759 G ∧ Equation1152 G ∧ Equation1165 G ∧ Equation1171 G ∧ Equation1181 G ∧ Equation1293 G ∧ Equation1304 G ∧ Equation1320 G ∧ Equation1340 G ∧ Equation1358 G ∧ Equation1374 G ∧ Equation1467 G ∧ Equation1470 G ∧ Equation1504 G ∧ Equation1507 G ∧ Equation1561 G ∧ Equation1670 G ∧ Equation1699 G ∧ Equation1793 G ∧ Equation1876 G ∧ Equation1943 G ∧ Equation1983 G ∧ Equation2170 G ∧ Equation2180 G ∧ Equation2186 G ∧ Equation2196 G ∧ Equation2199 G ∧ Equation2271 G ∧ Equation2279 G ∧ Equation2335 G ∧ Equation2349 G ∧ Equation2373 G ∧ Equation2399 G ∧ Equation2482 G ∧ Equation2519 G ∧ Equation2522 G ∧ Equation2573 G ∧ ⋯