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 a b. a + b = 0 -> b = 0Every 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 a b. a + b = 0 -> b = 0Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
PA0006 beta_range_empty PA0007 mul_eq_zero PA000J add_eq_zero_left PA000N mul_eq_one_components PA0013 factor_difference PA001B le_zero PA002I bounded_beta_exclusive_recode_invariant PA003G beta_prefix_sum_trace_exists PA003W beta_prefix_product_trace_exists PA0043 beta_repeat_empty PA004F finite_surjective_zero PA004H finite_contains_decidable PA004J beta_prefix_replace_exists PA0052 beta_product_replace_balance PA005L quadratic_residue_search_up_to PA0074 gauss_signed_half_prefix_exists PA007D beta_magnitude_predecessor_recode_exists PA007G beta_sign_factor_prefix_exists PA007L beta_pointwise_mul_prefix_exists PA008B prime_mul_index_map_exists_up_to PA008C beta_successor_lift_exists PA008S prime_scaled_inverse_prefix_exists_bounded PA008U scaled_orbit_closed_prefix_zero PA008V bounded_into_zero PA008W injective_prefix_zero PA008Y adjacent_scaled_orbit_history_zero PA0092 finite_covers_into_or_omits PA0094 finite_inverse_choice_prefix_exists PA00A6 prime_inverse_prefix_exists_bounded PA00A8 orbit_closed_prefix_zero PA00A9 nonendpoint_prefix_zero PA00AB paired_inverse_witness_zero PA00BY beta_division_prefix_exists PA00CU beta_sum_replace_balance PA00DD eisenstein_row_indicator_prefix_exists PA00DJ eisenstein_rectangle_row_count_prefix_exists PA00E9 eisenstein_transposed_column_prefix_exists PA00EI eisenstein_transposed_column_count_prefix_exists PA00EX eisenstein_successor_row_split_prefix_existsDefinition-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 a
02Induction on bL2–5
03Separate the logical casesL6–6
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L6
exfalso
04Use earlier factsL7–7
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L7
apply PA1
05Calculate and transport equalitiesL8–8
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L8
rewrite PA4 at h
06Use earlier factsL9–9
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L9
exact h