structure Hex.ECPP.CM.ClassPolynomial : Type

A negative discriminant's absolute value and its monic Hilbert polynomial.

• d : Nat
• coefficients : List Int

def Hex.ECPP.CM.instReprClassPolynomial.repr : ClassPolynomial → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.ECPP.CM.instReprClassPolynomial : Repr ClassPolynomial

Equations

• Hex.ECPP.CM.instReprClassPolynomial = { reprPrec := Hex.ECPP.CM.instReprClassPolynomial.repr }

def Hex.ECPP.CM.classPolynomials : List ClassPolynomial

Thirty-three fixed linear/quadratic polynomials; no subject-specific data.

Equations

• One or more equations did not get rendered due to their size.