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.
Definition in prerequisite notation
∃ sph_inverse_secondwave. Lt(sph_inverse_secondwave,p) ∧ ModEq(p,dp · sph_inverse_secondwave,1 + dn · sph_inverse_secondwave)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists sph_inverse_secondwave. ((exists hpl_gap_secondwave. hpl_gap_secondwave + S (sph_inverse_secondwave) = (p)) /\ (exists hgcrt_mod_left_hpl_secondwave hgcrt_mod_right_hpl_secondwave. (dp * sph_inverse_secondwave) + p * hgcrt_mod_left_hpl_secondwave = (1 + dn * sph_inverse_secondwave) + p * hgcrt_mod_right_hpl_secondwave))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
Checked theorems using this definition
HL001A · hensel_signed_blend_unit_coprimeHL001D · hensel_signed_derivative_unit_mod_transportHL001E · beta_signed_horner_lift_preserves_simplicityHL001F · beta_signed_horner_hensel_iterated_exists_uniqueHL0020 · beta_signed_horner_simple_root_hensel_lift_exists_uniqueHL0021 · beta_signed_horner_prime_power_hensel_lift_exists_uniqueHL0022 · beta_signed_horner_prime_power_iterated_lifts_exists_uniqueHL0025 · hensel_prime_blended_nonzero_derivative_is_unitHL0026 · hensel_prime_signed_nonzero_derivative_is_unit