This file is generated from the following refutation as produced by random generation of polynomials: '(0 * x2 + 0 * y2 + 4 * x + 2 * y + 0 * x * y) % 5' (0, 2, 7, 22, 25, 46, 64, 72, 98, 101, 116, 124, 150, 159, 166, 202, 211, 228, 254, 257, 262, 306, 325, 334, 358, 361, 374, 410, 428, 436, 463, 472, 503, 512, 545, 561, 613, 616, 631, 639, 678, 703, 816, 825, 832, 871, 878, 909, 916, 948, 961, 1019, 1028, 1045, 1075, 1084, 1109, 1118, 1222, 1225, 1230, 1277, 1322, 1425, 1454, 1481, 1490, 1517, 1525, 1628, 1631, 1653, 1657, 1661, 1681, 1720, 1728, 1789, 1831, 1837, 1849, 1860, 1872, 1884, 1896, 1924, 1966, 2034, 2043, 2052, 2059, 2099, 2124, 2237, 2266, 2293, 2299, 2327, 2329, 2440, 2448, 2456, 2469, 2484, 2502, 2532, 2540, 2585, 2643, 2652, 2662, 2671, 2698, 2743, 2846, 2849, 2862, 2874, 2909, 2938, 3049, 3052, 3057, 3065, 3074, 3078, 3082, 3093, 3112, 3252, 3270, 3278, 3318, 3342, 3351, 3455, 3458, 3473, 3481, 3517, 3521, 3525, 3557, 3606, 3658, 3667, 3674, 3714, 3721, 3760, 3861, 3870, 3887, 3914, 3923, 3953, 4064, 4067, 4072, 4117, 4126, 4130, 4134, 4145, 4156, 4289, 4320, 4368, 4379, 4382, 4407, 4434, 4442, 4469, 4584, 4635, 4655)

The magma definition

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

Equations

• «FinitePoly 4 * x + 2 * y % 5» = { op := MemoFinOp.opOfTable 263799205844014610 }

The facts

theorem «Facts from FinitePoly 4 * x + 2 * y % 5» : ∃ (G : Type) (x : Magma G) (_ : Finite G), Equation65 G ∧ Equation73 G ∧ Equation102 G ∧ Equation117 G ∧ Equation125 G ∧ Equation160 G ∧ Equation167 G ∧ Equation212 G ∧ Equation229 G ∧ Equation258 G ∧ Equation263 G ∧ Equation335 G ∧ Equation362 G ∧ Equation437 G ∧ Equation546 G ∧ Equation562 G ∧ Equation617 G ∧ Equation632 G ∧ Equation640 G ∧ Equation679 G ∧ Equation704 G ∧ Equation826 G ∧ Equation949 G ∧ Equation962 G ∧ Equation1029 G ∧ Equation1046 G ∧ Equation1076 G ∧ Equation1085 G ∧ Equation1110 G ∧ Equation1119 G ∧ Equation1226 G ∧ Equation1231 G ∧ Equation1278 G ∧ Equation1323 G ∧ Equation1455 G ∧ Equation1482 G ∧ Equation1491 G ∧ Equation1518 G ∧ Equation1526 G ∧ Equation1721 G ∧ Equation1790 G ∧ Equation1897 G ∧ Equation1967 G ∧ Equation2044 G ∧ Equation2053 G ∧ Equation2060 G ∧ Equation2100 G ∧ Equation2125 G ∧ ⋯