Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Definition in prerequisite notation
Lt(1,m) ∧ (∃ x. Lt(x,m) ∧ ModEq(m,a · x,1))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
(exists eut_gap_eu_bottomlayer_domain. eut_gap_eu_bottomlayer_domain + S (1) = ((m))) /\ exists eu_inverse_bottomlayer. (exists eut_gap_eu_bottomlayer_bound. eut_gap_eu_bottomlayer_bound + S (eu_inverse_bottomlayer) = ((m))) /\ (exists eu_mod_left_bottomlayer_inverse eu_mod_right_bottomlayer_inverse. (((a))*eu_inverse_bottomlayer) + ((m)) * eu_mod_left_bottomlayer_inverse = (1) + ((m)) * eu_mod_right_bottomlayer_inverse)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
none