Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Definition in prerequisite notation
(L = 0 ∨ M = 0) ∧ N = 0 ∨ ¬L = 0 ∧ (¬M = 0 ∧ L + M = S N)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
(((((L))=0 \/ ((M))=0) /\ ((((N))=0)))) \/ (((~(((L))=0)) /\ (((~(((M))=0)) /\ ((((L))+((M))=S ((N))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
none — first-order arithmetic only
Definitions depending on this notation
Checked theorems using this definition
PG0009 · polynomial_product_length_shift_right_nonemptyPG000D · prime_field_polynomial_convolution_shift_right_existsPG001F · prime_field_polynomial_convolution_right_append_existsPG0021 · prime_field_polynomial_convolution_shift_scale_aligned_equivalentPG0023 · prime_field_polynomial_convolution_associativity_append_stepPG0025 · prime_field_polynomial_convolution_associative_equivalentPG002B · prime_field_polynomial_right_divides_equivalent_divisorPG002C · prime_field_polynomial_right_divides_transitivePG0058 · prime_field_polynomial_right_divides_aligned_addPG0059 · prime_field_polynomial_right_divides_aligned_subtractPG005E · prime_field_polynomial_bezout_euclidean_backwardPG0062 · prime_field_polynomial_bezout_equivalent_transportPG006F · prime_field_polynomial_product_equivalent_nonzero_left_nonemptyPG0070 · prime_field_polynomial_right_divides_represented_factorizationPG0075 · prime_field_polynomial_empty_right_divisor_implies_equivalent_zero