ND0335

PolynomialPowerCoefficient(b,c,L,k,a)

The actual coefficient of X^k is decoded at the index i with i+S k=L, or is zero when L<=k. Empty representations therefore have every formal coefficient zero. This is a coefficient of a formal polynomial, not its value at a field element.

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

(∃ x. x + S k = L ∧ BetaAt(b,c,x,a)) ∨ Le(L,k) ∧ a = 0

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

Hygienic expanded first-order definition 
(exists pfrep_position_working_euclidean_definition. ((pfrep_position_working_euclidean_definition+S ((k))=((L))) /\ ((((exists ff_h_pfp_working_euclidean_definitionentry. ff_h_pfp_working_euclidean_definitionentry + S ((a)) = S ((S (pfrep_position_working_euclidean_definition)) * (c))) /\ exists ff_q_pfp_working_euclidean_definitionentry. (b) = ff_q_pfp_working_euclidean_definitionentry * S ((S (pfrep_position_working_euclidean_definition)) * (c)) + ((a))))))) \/ (((exists pfrep_gap_working_euclidean_definitionoutside. pfrep_gap_working_euclidean_definitionoutside+((L))=((k))) /\ ((((a))=0))))

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

Direct definition dependencies

BetaAt(b,c,i,x)Le(a,b)

Definitions depending on this notation

PolynomialEquivalent(b,c,L,d,e,M)

Checked theorems using this definition

PX000C · prime_field_polynomial_power_coefficient_existsPX000E · prime_field_polynomial_power_coefficient_transportPX0010 · prime_field_polynomial_equivalent_transitivePX001A · prime_field_polynomial_left_pad_power_coefficientPX0021 · prime_field_polynomial_zero_power_coefficient