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
∃ u. ∃ v. a + m · u = b + m · vOnly definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists u v. a + m * u = b + m * vThe unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
none — first-order arithmetic only
Definitions depending on this notation
HornerRootModulo(b,c,a,l,m)SimpleHornerRoot(b,c,a,l,m,p)CanonicalHornerLift(b,c,l,m,a,M,r)SignedDerivativeUnit(p,dp,dn)SignedHornerRoot(pb,pc,nb,nc,a,l,m)SignedSimpleHornerRoot(pb,pc,nb,nc,a,l,m,p)CanonicalSignedHornerLift(pb,pc,nb,nc,l,m,a,M,r)SignedDerivativeNonzero(p,dp,dn)SignedNonsingularHornerRoot(pb,pc,nb,nc,a,l,m,p)
Checked theorems using this definition
HL0001 · hensel_mod_add_zero_cancelHL0002 · hensel_coprime_mod_transportHL0003 · hensel_canonical_residue_existsHL0005 · hensel_canonical_lift_digit_decomposeHL0007 · hensel_lift_correction_of_rootHL0008 · hensel_canonical_horner_lift_exists_uniqueHL0009 · beta_horner_simple_canonical_representativeHL000A · beta_horner_simple_root_hensel_lift_exists_uniqueHL000B · beta_horner_root_mod_transportHL000D · beta_horner_simple_root_at_congruent_pointHL000E · hensel_canonical_horner_root_exists_uniqueHL0010 · beta_horner_prime_power_hensel_lift_exists_uniqueHL0012 · beta_horner_hensel_iterated_exists_uniqueHL0013 · beta_horner_prime_power_iterated_lifts_exists_uniqueHL0018 · hensel_signed_blend_mod_iffHL0019 · hensel_signed_blend_zero_iffHL001A · hensel_signed_blend_unit_coprimeHL001B · beta_signed_horner_blend_root_equivalenceHL001C · beta_signed_horner_root_value_derivative_existsHL001D · 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_unit