Module MakeAllPrime.FieldProperties

val zero_nullifier_random : unit -> unit
val zero_nullifier_zero : unit -> unit
val zero_nullifier_one : unit -> unit
val inverse_property : unit -> unit
val inverse_of_one_is_one : unit -> unit
val zero_has_no_inverse : unit -> unit
val inverse_of_non_null_does_exist : unit -> unit
val inverse_of_inverse : unit -> unit
val opposite_property : unit -> unit
val opposite_of_opposite : unit -> unit
val opposite_of_zero_is_zero : unit -> unit
val additive_associativity : unit -> unit
val distributivity : unit -> unit
val multiplicative_associativity : unit -> unit
val pow_zero_to_zero_is_one : unit -> unit
val pow_zero_to_non_null_exponent_is_zero : unit -> unit
val pow_zero_on_random_equals_one : unit -> unit
val pow_zero_on_one_equals_one : unit -> unit
val pow_one_on_random_element_equals_the_random_element : unit -> unit
val pow_two_on_random_element_equals_the_square : unit -> unit
val pow_to_negative_exponent : unit -> unit
val pow_addition_property : unit -> unit
val pow_to_the_additive_group_order_equals_same_element : unit -> unit
val pow_to_the_multiplicative_group_order_equals_one : unit -> unit
val pow_add_multiplicative_group_order_to_a_random_power : unit -> unit
val sub_definition : unit -> unit
val get_tests : unit -> string * unit Alcotest.test_case list