PA000M — one

Exact expanded PA statement

forall n. 1 * n = n

Structural proof guide

Generated structural guide

One is a left identity for multiplication.

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

The proof proceeds by structural induction (1), certified simplification (2).

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA000N mul_eq_one_components PA001P gauss_coprime_cancel PA002N le_scaled_nonzero PA003G beta_prefix_sum_trace_exists PA003W beta_prefix_product_trace_exists PA005E pow_predecessor_parity_mod PA005T pow_one_from_zero_successor PA00AK bounded_mod_inverse_unique PA007N beta_product_pointwise_mul_exact PA007Q beta_product_pointwise_scale_mod PA00AO inverse_prefix_zero_fixed PA00B9 beta_adjacent_unit_pairs_product_one PA00BI mod_one_product_restore_predecessor PA00DQ odd_half_cross_product_gap

Formal 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.