This file is generated from the following refutation as produced by random generation of polynomials: '(0 * x2 + 1 * y2 + 3 * x + 0 * y + 2 * x * y) % 4' (0, 1831, 1834, 1856, 1860, 1864, 2034, 2037, 2050, 2052, 2846, 2852, 2862, 2871, 3049, 3055, 3067, 3078, 3090, 3252, 3255, 3258, 3260, 3305, 3307, 3314, 3318, 3322, 3330, 3333, 3455, 3458, 3461, 3463, 3508, 3510, 3517, 3521, 3525, 3533, 3536, 3658, 3661, 3711, 3713, 4269, 4282, 4340, 4357, 4379, 4395, 4432, 4468)

The magma definition

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

Equations

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

The facts

theorem «Facts from FinitePoly y² + 3 * x + 2 * x * y % 4» : ∃ (G : Type) (x : Magma G) (_ : Finite G), Equation1865 G ∧ Equation2038 G ∧ Equation2051 G ∧ Equation2053 G ∧ Equation2853 G ∧ Equation2863 G ∧ Equation2872 G ∧ Equation3323 G ∧ Equation3331 G ∧ Equation3334 G ∧ Equation3526 G ∧ Equation3537 G ∧ Equation3662 G ∧ Equation3712 G ∧ Equation3714 G ∧ Equation4358 G ∧ Equation4396 G ∧ Equation4433 G ∧ Equation4469 G ∧ ¬Equation47 G ∧ ¬Equation99 G ∧ ¬Equation151 G ∧ ¬Equation203 G ∧ ¬Equation255 G ∧ ¬Equation307 G ∧ ¬Equation411 G ∧ ¬Equation614 G ∧ ¬Equation817 G ∧ ¬Equation1020 G ∧ ¬Equation1223 G ∧ ¬Equation1426 G ∧ ¬Equation1629 G ∧ ¬Equation1833 G ∧ ¬Equation1834 G ∧ ¬Equation1837 G ∧ ¬Equation1838 G ∧ ¬Equation1840 G ∧ ¬Equation1841 G ∧ ¬Equation1847 G ∧ ¬Equation1848 G ∧ ¬Equation1850 G ∧ ¬Equation1851 G ∧ ¬Equation1858 G ∧ ¬Equation1860 G ∧ ¬Equation1884 G ∧ ¬Equation1885 G ∧ ¬Equation1887 G ∧ ¬Equation1888 G ∧ ⋯