BT000A

mul_one

Stable · empty-context checked

One is a right identity for multiplication.

Exact expanded PA statement

forall n. n * 1 = n

Structural proof guide

One is a right identity for multiplication.

Direct prerequisites: zero_add. The authored body proceeds by direct introduction and elimination.

Proof neighborhood

Direct dependencies

BT0000 zero_add

Direct dependents

BT0028 multiple_refl BT002F multiple_antisymm BT003J proper_factor_lt BT003M prime_divisor_eq_one_or_self BT004F binary_crt BT009X pow_add BT00PW le_mul_of_one_le_right BT00QE succ_le_mul_of_two_le_right BT00QU two_mul_eq_add_self BT00QV pow_mul_base BT00TX choose_factorial_bridge BT00UQ beta_product_prefix_suffix_split BT00Y8 division_quotient_one_of_bounds BT00Y9 division_quotient_two_of_bounds BT00YA prime_square_tail_of_two_three_range BT0104 prime_contribution_reverse_divides BT010U beta_product_all_one_exact BT0113 central_binom_factorization_small

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. 0002simp [zero_add]