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 · cp + an · cn + (bp · dn + bn · dp) + rn = rp + (ap · cn + an · cp + (bp · dp + bn · dn)) ∧ ap · dp + an · dn + (bp · cp + bn · cn) + (bp · dn + bn · dp) + sn = sp + (ap · dn + an · dp + (bp · cn + bn · cp) + (bp · dp + bn · dn))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
(((((((((ap) * (cp))) + (((an) * (cn))))) + (((((bp) * (dn))) + (((bn) * (dp))))))) + (rn)) = ((rp) + (((((((ap) * (cn))) + (((an) * (cp))))) + (((((bp) * (dp))) + (((bn) * (dn))))))))) /\ (((((((((((ap) * (dp))) + (((an) * (dn))))) + (((((bp) * (cp))) + (((bn) * (cn))))))) + (((((bp) * (dn))) + (((bn) * (dp))))))) + (sn)) = ((sp) + (((((((((ap) * (dn))) + (((an) * (dp))))) + (((((bp) * (cn))) + (((bn) * (cp))))))) + (((((bp) * (dp))) + (((bn) * (dn)))))))))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
none
Checked theorems using this definition
EI0022 · eisenstein_product_differenceEI0023 · eisenstein_product_integer_congruenceEI0024 · eisenstein_omega_product_covarianceEI0025 · eisenstein_product_associate_imaginaryEI0026 · eisenstein_product_associateEI0028 · eisenstein_conjugate_product_is_normEI0029 · eisenstein_natural_scalar_productEI002A · eisenstein_adjoint_product_is_norm_scaleEI002B · eisenstein_residual_conjugate_identityEI002C · eisenstein_product_commuteEI002E · eisenstein_product_shuffleEI002F · eisenstein_coordinate_norm_productEI0033 · eisenstein_signed_euclidean_division_exists