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. 0 * n = 0Structural proof guide
Generated structural guide
Zero annihilates multiplication on the left.
This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.
The proof proceeds by structural induction (1), certified simplification (2).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct dependents
PA000H mul_comm PA000N mul_eq_one_components PA0031 prime_nonzero PA0034 beta_half_range_entry_bounds PA003E beta_at_self_of_bound PA006Y odd_upper_remainder_reflection PA007C gauss_signed_half_magnitude_injective PA00A2 prime_two_or_terminal_odd_shape PA00C2 odd_half_strictly_below_modulus PA00EK beta_repeat_sum_exact PA00ES eisenstein_zero_width_rectangle_sum_zeroFormal native tactic body
Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.
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.