pith. machine review for the scientific record. sign in
def definition def or abbrev

hasseBound

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  44def hasseBound (q : ℕ) (a : ℤ) : Prop :=

proof body

Definition body.

  45  ((a : ℝ) ^ 2) ≤ 4 * (q : ℝ)
  46
  47/-! ## The Hilbert--Pólya operator -/
  48
  49/-- The Hilbert--Pólya operator `T_E` for an elliptic curve `E / F_q` with
  50    Frobenius trace `a`.  This is the real symmetric `2 × 2` matrix
  51    `[[0, θ], [θ, 0]]` where `θ` is the Frobenius angle. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.