# Generated by tools/translator: qualified upstream name -> MoonBit name.
CONG_TO_1_POW2 cong_to_1_pow2
COPRIME_1_PLUS_POWER coprime_1_plus_power
COPRIME_1_PLUS_POWER_STEP coprime_1_plus_power_step
COUNT_ORDERS_MODULO_PRIME count_orders_modulo_prime
COUNT_POWER_RESIDUES_MODULO_PRIMITIVE count_power_residues_modulo_primitive
COUNT_PRIMITIVE_ROOTS count_primitive_roots
COUNT_PRIMITIVE_ROOTS_ALT count_primitive_roots_alt
COUNT_QUADRATIC_RESIDUES_MODULO_PRIMITIVE count_quadratic_residues_modulo_primitive
COUNT_ROOTS_MODULO_ODD count_roots_modulo_odd
COUNT_ROOTS_MODULO_ODD_ALT count_roots_modulo_odd_alt
COUNT_ROOTS_MODULO_ODD_ALT_GEN count_roots_modulo_odd_alt_gen
COUNT_ROOTS_MODULO_ODD_GEN count_roots_modulo_odd_gen
COUNT_ROOTS_MODULO_PRIMITIVE count_roots_modulo_primitive
COUNT_ROOTS_MODULO_PRIMITIVE_ALT count_roots_modulo_primitive_alt
COUNT_ROOTS_MODULO_PRIMITIVE_GEN count_roots_modulo_primitive_gen
COUNT_ROOTS_MODULO_PRIMITIVE_GEN_ALT count_roots_modulo_primitive_gen_alt
EULER_CRITERION euler_criterion
FINITE_INTSEG_RESTRICT finite_intseg_restrict
GENERALIZED_EULER_CRITERION generalized_euler_criterion
GENERALIZED_EULER_CRITERION_PRIME generalized_euler_criterion_prime
INJECTIVE_EXP_MODULO_EQ injective_exp_modulo_eq
INT_OF_NUM_POWER_RESIDUE int_of_num_power_residue
INT_POLY_DIFF_EXPLICIT int_poly_diff_explicit
INT_POLY_LAGRANGE int_poly_lagrange
INT_PRIME int_prime
NO_PRIMITIVE_ROOT_MODULO_COMPOSITE no_primitive_root_modulo_composite
NO_PRIMITIVE_ROOT_MODULO_POW2 no_primitive_root_modulo_pow2
NUM_LAGRANGE_LEMMA num_lagrange_lemma
POWER_RESIDUE_EXISTS power_residue_exists
POWER_RESIDUE_MODULO_EQ power_residue_modulo_eq
POWER_RESIDUE_MODULO_EQ_ALT power_residue_modulo_eq_alt
POWER_RESIDUE_MODULO_ODD power_residue_modulo_odd
POWER_RESIDUE_MODULO_PRIME_EQ power_residue_modulo_prime_eq
POWER_RESIDUE_MODULO_PRIMITIVE power_residue_modulo_primitive
POWER_RESIDUE_MODULO_PRIMITIVE_ORDER power_residue_modulo_primitive_order
POWER_RESIDUE_MODULO_PRIMITIVE_ORDER_ALT power_residue_modulo_primitive_order_alt
POWER_RESIDUE_MODULO_PRIMITIVE_POWER power_residue_modulo_primitive_power
PRIME_DIVISOR_ORDER_EXISTS prime_divisor_order_exists
PRIMITIVE_ROOTS_MODULO_PRIME primitive_roots_modulo_prime
PRIMITIVE_ROOT_DOUBLE_LEMMA primitive_root_double_lemma
PRIMITIVE_ROOT_EXISTS primitive_root_exists
PRIMITIVE_ROOT_EXISTS_NONTRIVIAL primitive_root_exists_nontrivial
PRIMITIVE_ROOT_MODULO_0 primitive_root_modulo_0
PRIMITIVE_ROOT_MODULO_1 primitive_root_modulo_1
PRIMITIVE_ROOT_MODULO_2 primitive_root_modulo_2
PRIMITIVE_ROOT_MODULO_4 primitive_root_modulo_4
PRIMITIVE_ROOT_MODULO_DOUBLE_PRIMEPOW primitive_root_modulo_double_primepow
PRIMITIVE_ROOT_MODULO_PRIME primitive_root_modulo_prime
PRIMITIVE_ROOT_MODULO_PRIMEPOW primitive_root_modulo_primepow
PRIMITIVE_ROOT_MODULO_PRIMEPOWS primitive_root_modulo_primepows
QUADRATIC_NONRESIDUE_EXISTS quadratic_nonresidue_exists
QUADRATIC_RESIDUE_MODULO_ODD_POWER quadratic_residue_modulo_odd_power
QUADRATIC_RESIDUE_MODULO_POWER_2 quadratic_residue_modulo_power_2
QUADRATIC_RESIDUE_MODULO_POWER_2_STABLE quadratic_residue_modulo_power_2_stable
QUADRATIC_RESIDUE_MODULO_PRIMITIVE_ORDER quadratic_residue_modulo_primitive_order
QUADRATIC_RESIDUE_MODULO_PRIMITIVE_POWER quadratic_residue_modulo_primitive_power
REAL_POLY_DIFF_EXPLICIT real_poly_diff_explicit
