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.
Exact expanded PA statement
forall n. n * 1 = nStructural proof guide
One is a right identity for multiplication.
Direct prerequisites: zero_add. The authored body proceeds by direct introduction and elimination.
Proof neighborhood
Direct dependencies
Direct 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_smallFormal native tactic body
Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.
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.