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
cp · qp + cn · qn + (dp · un + dn · up) + rp + an = ap + (cp · qn + cn · qp + (dp · up + dn · un) + rn) ∧ cp · up + cn · un + (dp · qp + dn · qn) + (dp · un + dn · up) + sp + bn = bp + (cp · un + cn · up + (dp · qn + dn · qp) + (dp · up + dn · un) + sn) ∧ (EisensteinCoordinateNorm(rp,rn,sp,sn,U) ∧ (EisensteinCoordinateNorm(cp,cn,dp,dn,V) ∧ Lt(U,V)))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((((((((((((((cp) * (qp))) + (((cn) * (qn))))) + (((((dp) * (un))) + (((dn) * (up))))))) + (rp))) + (an)) = ((ap) + (((((((((cp) * (qn))) + (((cn) * (qp))))) + (((((dp) * (up))) + (((dn) * (un))))))) + (rn))))) /\ (((((((((((((cp) * (up))) + (((cn) * (un))))) + (((((dp) * (qp))) + (((dn) * (qn))))))) + (((((dp) * (un))) + (((dn) * (up))))))) + (sp))) + (bn)) = ((bp) + (((((((((((cp) * (un))) + (((cn) * (up))))) + (((((dp) * (qn))) + (((dn) * (qp))))))) + (((((dp) * (up))) + (((dn) * (un))))))) + (sn))))))) /\ ((((((((((rp) * (rp))) + (((rn) * (rn))))) + (((((sp) * (sp))) + (((sn) * (sn))))))) + (((((rp) * (sn))) + (((rn) * (sp)))))) = ((((((((((rp) * (rn))) + (((rn) * (rp))))) + (((((sp) * (sn))) + (((sn) * (sp))))))) + (((((rp) * (sp))) + (((rn) * (sn))))))) + (U))) /\ ((((((((((cp) * (cp))) + (((cn) * (cn))))) + (((((dp) * (dp))) + (((dn) * (dn))))))) + (((((cp) * (dn))) + (((cn) * (dp)))))) = ((((((((((cp) * (cn))) + (((cn) * (cp))))) + (((((dp) * (dn))) + (((dn) * (dp))))))) + (((((cp) * (dp))) + (((cn) * (dn))))))) + (V))) /\ (exists ee_gap_lowerlayer. ee_gap_lowerlayer + S (U) = (V)))))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