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 k. (n + m) * k = n * k + m * kEvery 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 m k. (n + m) * k = n * k + m * kProof neighborhood
Direct theorem prerequisites
Direct theorem dependents
BT001M mul_le_mul_right BT0033 balanced_bezout_euclid_step BT0036 balanced_combination_scale_right BT003S mod_eq_mul_right BT004J common_divisor_beta_moduli_divides_gap_times_c BT00R4 square_six_shift_identity BT00U0 four_power_central_recurrence_step BT00W4 pow_three_five_le_pow_four_four_from_total BT00W5 pow_eleven_two_le_pow_two_seven_from_total BT00W7 linear_square_budget BT00W9 bertrand_scaled_budget_root_33 BT00WA bertrand_scaled_budget_root_34 BT00WB bertrand_scaled_budget_root_35 BT00WC bertrand_scaled_budget_root_36 BT00WD bertrand_scaled_budget_root_37 BT00WQ bertrand_h_root_33_from_total BT011N prime_five_hundred_twenty_one BT0120 bertrand_cover_eighty_three_one_hundred_sixty_three BT0121 bertrand_cover_one_hundred_sixty_three_three_hundred_seventeen BT0122 bertrand_cover_three_hundred_seventeen_five_hundred_twenty_one BT0123 bertrand_cutoff_lt_final_primeDefinition-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.
01Fix variables and assumptionsL1–3
02Calculate and transport equalitiesL4–4
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L4
simp [mul_comm, mul_add]