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 m. S n * m = n * m + mEvery purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.
Definitions used by this theorem
In the theorem statement
0 occurrences
In local proof propositions
0 occurrences
Exact expanded native-PA statement
forall n m. S n * m = n * m + mProof neighborhood
Direct theorem prerequisites
Direct theorem dependents
PA000H mul_comm PA0025 mod_eq_predecessor_cancel PA002P base_le_beta_modulus PA0034 beta_half_range_entry_bounds PA005D predecessor_square_mod_one PA006Y odd_upper_remainder_reflection PA0070 gauss_pointwise_signed_half_representative PA007B gauss_mixed_sign_scaled_source_impossible PA007C gauss_signed_half_magnitude_injective PA00A2 prime_two_or_terminal_odd_shape PA00AG prime_bounded_square_one_cases PA00C2 odd_half_strictly_below_modulus PA00C4 predecessor_multiple_mod_complement PA00DQ odd_half_cross_product_gap PA00EK beta_repeat_sum_exactDefinition-aware tactic body
Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.
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.
Named ingredients (1)
01Fix variables and assumptionsL1–1
Work with arbitrary variables or the premises of the current implication.
- L1
intro n