This file is generated from the following refutation as produced by random generation of polynomials: '(0 * x2 + 0 * y2 + 0 * x + 1 * y + 1 * x * y) % 3' (0, 2440, 2442, 2542, 2643, 2645, 2745, 3252, 3305, 4319, 4361)

The magma definition

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

Equations

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

The facts

theorem «Facts from FinitePoly y + x * y % 3» : ∃ (G : Type) (x : Magma G) (_ : Finite G), Equation2443 G ∧ Equation2543 G ∧ Equation2646 G ∧ Equation2746 G ∧ Equation3306 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 ∧ ¬Equation1832 G ∧ ¬Equation2035 G ∧ ¬Equation2238 G ∧ ¬Equation2442 G ∧ ¬Equation2444 G ∧ ¬Equation2446 G ∧ ¬Equation2447 G ∧ ¬Equation2449 G ∧ ¬Equation2450 G ∧ ¬Equation2456 G ∧ ¬Equation2457 G ∧ ¬Equation2459 G ∧ ¬Equation2460 G ∧ ¬Equation2466 G ∧ ¬Equation2467 G ∧ ¬Equation2469 G ∧ ¬Equation2470 G ∧ ¬Equation2493 G ∧ ¬Equation2494 G ∧ ¬Equation2496 G ∧ ¬Equation2497 G ∧ ¬Equation2503 G ∧ ¬Equation2504 G ∧ ¬Equation2506 G ∧ ¬Equation2507 G ∧ ¬Equation2530 G ∧ ¬Equation2531 G ∧ ¬Equation2533 G ∧ ¬Equation2534 G ∧ ¬Equation2540 G ∧ ⋯