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. n * m = m * nEvery 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. n * m = m * nProof neighborhood
Direct theorem prerequisites
Direct theorem 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_oddDefinition-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.
01Fix variables and assumptionsL1–1
Work with arbitrary variables or the premises of the current implication.
- L1
intro n