Readable signature
Even(n)Exact expansion
exists h. n = 2 * hThis node is notation, not a theorem, axiom, predicate constant, or kernel rule. The elaboration layer must expand it before proof checking.
Definition neighborhood
Expands using
none
Used by definitions
none
Used by theorem statements or local proof propositions
PA0056 odd_not_even PA0058 successor_odd_of_even PA0059 even_not_odd PA005A even_successor_to_odd PA005B successor_even_of_odd PA005C odd_successor_to_even PA005E pow_predecessor_parity_mod PA006E even_mul_right PA006F even_add_odd PA006G odd_add_even PA006H even_add_even PA006I odd_add_odd PA006U even_mul_left PA00BV arbitrary_gauss_lemma_complete PA00C7 odd_multiplier_even_product_iff PA00C8 odd_multiplier_odd_product_iff PA00C9 odd_multiplier_parity_iff PA00CA even_sum_parity_cases PA00CB even_sum_iff_same_parity PA00CC odd_division_even_iff PA00CD odd_sum_parity_cases PA00CE odd_sum_iff_opposite_parity PA00CF odd_division_odd_iff PA00CG odd_division_parity_iff PA00CH even_to_mod_two_zero PA00CJ matching_parity_mod_two PA00CK odd_product_division_mod_two PA00D4 mod_two_zero_to_even PA00D5 mod_two_zero_sum_to_congruent PA00D7 odd_prime_gauss_eisenstein_orientation_data_exists PA00FG distinct_odd_primes_gauss_eisenstein_data_exists PA00FJ odd_half_even_iff_mod4_one PA00FL mod_two_preserves_parity PA00FM qres_same_status_from_even_count_sum PA00FN qres_same_status_from_even_half_product_mod_two PA00FO qres_same_status_from_mod_four_one PA00FP conditional_qres_same_status_from_oriented_gauss_counts PA00FS qres_opposite_status_from_odd_count_sum PA00FT qres_opposite_status_from_odd_half_product_mod_two PA00FU qres_opposite_status_from_mod_four_three PA00FV conditional_qres_opposite_status_from_oriented_gauss_counts PA00FW quadratic_reciprocity_combined