BT000B

add_mul

Stable · empty-context checked

Multiplication distributes over addition on the left.

Exact expanded PA statement

forall n m k. (n + m) * k = n * k + m * k

Structural proof guide

Multiplication distributes over addition on the left.

Direct prerequisites: mul_comm, mul_add. The authored body proceeds by direct introduction and elimination.

Proof neighborhood

Direct dependencies

BT0006 mul_comm BT0007 mul_add

Direct 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_prime

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro n
  2. 0002intro m
  3. 0003intro k
  4. 0004simp [mul_comm, mul_add]