def definition def or abbrev

`frobeniusAngle`

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

formal statement (Lean)

  40def frobeniusAngle (q : ℕ) (a : ℤ) : ℝ :=

Definition body.

  41  Real.arccos ((a : ℝ) / (2 * Real.sqrt (q : ℝ)))
  42
  43/-- The Hasse--Weil bound: `a^2 ≤ 4 q`, equivalently `|a| ≤ 2 √q`. -/

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

hilbert_polya_elliptic_curve in IndisputableMonolith.NumberTheory.HilbertPolyaFunctionField decl_use
hpOperator in IndisputableMonolith.NumberTheory.HilbertPolyaFunctionField decl_use
hpOperator_eigenvector_neg in IndisputableMonolith.NumberTheory.HilbertPolyaFunctionField decl_use
hpOperator_eigenvector_pos in IndisputableMonolith.NumberTheory.HilbertPolyaFunctionField decl_use