BT0006

mul_comm

Stable · empty-context checked

Multiplication is commutative.

Exact expanded PA statement

forall n m. n * m = m * n

Structural proof guide

Multiplication is commutative.

Direct prerequisites: mul_zero_left, mul_succ_left. The authored body proceeds by structural induction (1).

Proof neighborhood

Direct dependencies

BT0004 mul_zero_left BT0005 mul_succ_left

Direct dependents

BT000B add_mul BT002B multiple_mul_left BT0036 balanced_combination_scale_right BT003T mod_eq_mul_left BT003X mod_eq_to_remainder_decomposition BT0041 beta_at_exists BT0042 beta_at_unique BT004F binary_crt BT004I beta_modulus_coprime_base BT004K beta_moduli_coprime_of_gap_dvd BT004M bounded_common_multiple_step BT004V right_factor_divides_product BT0069 beta_factor_divides_product BT00BG coprime_product_is_lcm BT00QJ mul_shuffle_four BT00QU two_mul_eq_add_self BT00QV pow_mul_base BT00R4 square_six_shift_identity BT00RE three_mul_eq_two_mul_add_self BT00TW factorial_weighted_product_combine BT00TY mul_lt_mul_right_nonzero BT00U0 four_power_central_recurrence_step BT00VK central_binom_strong_upper_step BT00VP central_binom_odd_middle_le_four_pow BT00VX central_binom_prime_divisor_le_double BT00WC bertrand_scaled_budget_root_36 BT00WD bertrand_scaled_budget_root_37 BT00WU bertrand_h_root_37_from_total BT00X4 bertrand_floor_power_product_le_h_from_total BT00X5 bertrand_four_power_product_le_of_sum_from_total BT0118 nonprime_has_small_prime_divisor_below_square BT011C scaled_remainder_lift 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. 0002induction m
  3. 0003simp [mul_zero_left]
  4. 0004simp [IH, mul_succ_left]