ND0230

FpMul(p,a,b,c)

Bounded operands and the actual canonical residue of their natural product; no multiplication law is assumed.

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

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(a,p) ∧ (Lt(b,p) ∧ CanonicalModularResidue(p,a · b,c))

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

Hygienic expanded first-order definition 
((exists pfa_gap_bottomlayerleft. pfa_gap_bottomlayerleft + S ((a)) = ((p))) /\ (((exists pfa_gap_bottomlayerright. pfa_gap_bottomlayerright + S ((b)) = ((p))) /\ ((((exists pfa_gap_bottomlayerresultbound. pfa_gap_bottomlayerresultbound + S ((c)) = ((p))) /\ ((exists pfa_offset_left_bottomlayerresultcongruence pfa_offset_right_bottomlayerresultcongruence. (((a)) * ((b))) + ((p)) * pfa_offset_left_bottomlayerresultcongruence = ((c)) + ((p)) * pfa_offset_right_bottomlayerresultcongruence))))))))

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

Direct definition dependencies

Lt(a,b)CanonicalModularResidue(m,a,r)

Definitions depending on this notation

FpPolyScale(p,k,ab,ac,bb,bc,l)FpInv(p,a,b)FpPolynomialQuotientStep(p,k,ab,ac,bb,bc,M,qb,qc,i,q)

Checked theorems using this definition

PG0011 · polynomial_zero_extended_scale_congruentPG0014 · prime_field_convolution_coefficient_right_scalePG0018 · prime_field_polynomial_scale_zero_valuePG004F · prime_field_convolution_coefficient_left_constantPG0051 · prime_field_polynomial_scale_to_left_constant_productPG0072 · prime_field_polynomial_monic_singleton_multiple_equivalent