ND0228

FpElement(p,a)

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

A prime modulus and an actual canonical natural representative a<p. Field laws are proved separately.

Conservative notation; not a theorem, primitive, or axiom.

Definition in prerequisite notation

Prime(p) ∧ Lt(a,p)

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition 
((~(((p)) = 1) /\ forall pfa_factor_left_bottomlayerprime pfa_factor_right_bottomlayerprime. ((p)) = pfa_factor_left_bottomlayerprime * pfa_factor_right_bottomlayerprime -> pfa_factor_left_bottomlayerprime = 1 \/ pfa_factor_right_bottomlayerprime = 1) /\ ((exists pfa_gap_bottomlayerbound. pfa_gap_bottomlayerbound + S ((a)) = ((p)))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

Prime(p)Lt(a,b)

Definitions depending on this notation

none

Checked theorems using this definition

none directly; see definition consumers