ND0169 — EisensteinCoordinateNorm(ap,an,bp,bn,n)

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

ap · ap + an · an + (bp · bp + bn · bn) + (ap · bn + an · bp) = ap · an + an · ap + (bp · bn + bn · bp) + (ap · bp + an · bn) + n

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

Hygienic expanded first-order definition

((((((((ap) * (ap))) + (((an) * (an))))) + (((((bp) * (bp))) + (((bn) * (bn))))))) + (((((ap) * (bn))) + (((an) * (bp)))))) = ((((((((((ap) * (an))) + (((an) * (ap))))) + (((((bp) * (bn))) + (((bn) * (bp))))))) + (((((ap) * (bp))) + (((an) * (bn))))))) + (n))

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

Direct definition dependencies

none — first-order arithmetic only

Definitions depending on this notation

ENorm(z,n)EisensteinSignedDivisionRemainder(ap,an,bp,bn,cp,cn,dp,dn,qp,qn,up,un,rp,rn,sp,sn,U,V)

Checked theorems using this definition