finite_field.card_image_polynomial_eval

The cardinality of a field is at most n times the cardinality of the image of a degree n polnyomial

finite_field.exists_root_sum_quadratic

If f and g are quadratic polynomials, then the f.eval a + g.eval b = 0 has a solution.