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.
Statement with defined notation
forall n. n * 1 = nEvery purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.
Definitions used by this theorem
In the theorem statement
0 occurrences
In local proof propositions
0 occurrences
Exact expanded native-PA statement
forall n. n * 1 = nProof neighborhood
Direct theorem prerequisites
Direct theorem dependents
BT0028 multiple_refl BT002F multiple_antisymm BT003J proper_factor_lt BT003M prime_divisor_eq_one_or_self BT004F binary_crt BT009X pow_add BT00PW le_mul_of_one_le_right BT00QE succ_le_mul_of_two_le_right BT00QU two_mul_eq_add_self BT00QV pow_mul_base BT00TX choose_factorial_bridge BT00UQ beta_product_prefix_suffix_split BT00Y8 division_quotient_one_of_bounds BT00Y9 division_quotient_two_of_bounds BT00YA prime_square_tail_of_two_three_range BT0104 prime_contribution_reverse_divides BT010U beta_product_all_one_exact BT0113 central_binom_factorization_smallDefinition-aware tactic body
Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.