Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Readable signature
Odd(n)Exact expansion
exists h. n = 2 * h + 1This 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 PA0064 prime_ne_two_is_odd PA006D odd_mul_odd PA006F even_add_odd PA006G odd_add_even PA006I odd_add_odd PA00A2 prime_two_or_terminal_odd_shape 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 PA00CI odd_to_mod_two_one PA00CJ matching_parity_mod_two PA00CK odd_product_division_mod_two PA00CL odd_reflected_remainder_mod_two PA00CM signed_remainder_sum_mod_two PA00CN odd_scaled_division_signed_mod_two PA00CO odd_signed_division_congruence_mod_two PA00CP gauss_eisenstein_prefix_pointwise_mod_two PA00CR gauss_eisenstein_terminal_sums_mod_two PA00D3 gauss_eisenstein_terminal_cancel_magnitude_mod_two PA00D5 mod_two_zero_sum_to_congruent PA00D6 gauss_eisenstein_sign_count_mod_quotient_sum PA00D7 odd_prime_gauss_eisenstein_orientation_data_exists PA00FG distinct_odd_primes_gauss_eisenstein_data_exists PA00FK mod_two_one_to_odd 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 PA00FR odd_half_odd_iff_mod4_three 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