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
∃ mv_square_prime_bottomlayer. Prime(mv_square_prime_bottomlayer) ∧ Dvd(mv_square_prime_bottomlayer · mv_square_prime_bottomlayer,n)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists mv_square_prime_bottomlayer. ((~((mv_square_prime_bottomlayer) = 1) /\ forall pvs_left_bottomlayerprime pvs_right_bottomlayerprime. (mv_square_prime_bottomlayer) = pvs_left_bottomlayerprime * pvs_right_bottomlayerprime -> pvs_left_bottomlayerprime = 1 \/ pvs_right_bottomlayerprime = 1) /\ (exists pvs_factor_bottomlayerdivisor. ((n)) = (mv_square_prime_bottomlayer * mv_square_prime_bottomlayer) * pvs_factor_bottomlayerdivisor))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
none directly; see definition consumers