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 m. n * m = m * nStructural proof guide
Generated structural guide
Multiplication is commutative.
Use the direct prerequisites mul_zero_left, mul_succ_left as previously established PA formulas.
The proof proceeds by structural induction (1), certified simplification (2).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct dependents
PA000I bounded_common_multiple_step PA000T right_factor_divides_product PA0015 beta_modulus_coprime_base PA0016 add_mul PA001N balanced_combination_scale_right PA001Q beta_moduli_coprime_of_gap_dvd PA0020 mod_eq_mul_left PA0026 binary_crt PA0029 beta_at_exists PA002F beta_at_unique PA002V mod_eq_to_remainder_decomposition PA003C remainder_decomposition_to_mod_eq PA003Q coprime_mod_inverse PA003R mod_eq_cancel_coprime PA0052 beta_product_replace_balance PA005K mod_eq_decidable_nonzero PA005N square_decomp PA005R quadratic_residue_bounded_equiv PA0063 prime_bounded_nonzero_mod_inverse PA00AK bounded_mod_inverse_unique PA006C mul_double_right PA0072 gauss_half_range_signed_choices PA007N beta_product_pointwise_mul_exact PA007P gauss_signed_pointwise_mul_scale_mod PA007Q beta_product_pointwise_scale_mod PA0084 gauss_signed_products_cancel_mod PA0086 nondivisor_canonical_remainder_exists PA008A mod_eq_zero_to_dvd_nonzero PA008B prime_mul_index_map_exists_up_to PA008L fermat_predecessor_exponent_mod_one PA008N scaled_inverse_from_unit_inverse PA008Q prime_scaled_inverse_exists PA009B scaled_inverse_symmetric PA00AJ inverse_index_symmetric PA00BN bounded_euler_criterion_dichotomy PA00BO double_predecessor_ne_one PA00BV arbitrary_gauss_lemma_complete PA00C3 odd_half_positive_complement_exists PA00C5 canonical_remainder_from_mod PA00CL odd_reflected_remainder_mod_two PA00DQ odd_half_cross_product_gap PA00ES eisenstein_zero_width_rectangle_sum_zero PA00FK mod_two_one_to_oddFormal 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.
01Fix variables and assumptionsL1–1
Work with arbitrary variables or the premises of the current implication.
- L1
intro n