PA000D — mul_zero

Exact expanded PA statement

forall n. 0 * n = 0

Structural proof guide

Generated structural guide

Zero annihilates multiplication on the left.

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

PA000H mul_comm PA000N mul_eq_one_components PA0031 prime_nonzero PA0034 beta_half_range_entry_bounds PA003E beta_at_self_of_bound PA006Y odd_upper_remainder_reflection PA007C gauss_signed_half_magnitude_injective PA00A2 prime_two_or_terminal_odd_shape PA00C2 odd_half_strictly_below_modulus PA00EK beta_repeat_sum_exact PA00ES eisenstein_zero_width_rectangle_sum_zero

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.