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
Squarefree(r) ∧ n = r · (s · s)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((((~(((r)) = 0)) /\ (forall sfd_prime_prioritylayerkernel. (~((sfd_prime_prioritylayerkernel) = 1) /\ forall pvs_left_prioritylayerkerneldomain pvs_right_prioritylayerkerneldomain. (sfd_prime_prioritylayerkernel) = pvs_left_prioritylayerkerneldomain * pvs_right_prioritylayerkerneldomain -> pvs_left_prioritylayerkerneldomain = 1 \/ pvs_right_prioritylayerkerneldomain = 1) -> (exists pvs_le_gap_prioritylayerkernelbound. pvs_le_gap_prioritylayerkernelbound + (sfd_prime_prioritylayerkernel) = ((r))) -> ~(exists pvs_factor_prioritylayerkernelsquare. ((r)) = (sfd_prime_prioritylayerkernel * sfd_prime_prioritylayerkernel) * pvs_factor_prioritylayerkernelsquare)))) /\ (((n)) = ((r)) * (((s)) * ((s)))))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