rankOfDiscrBdd — Mathlib

English

If a number field K satisfies |discr K| ≤ N, then its degree over ℚ is bounded by rankOfDiscrBdd N, where rankOfDiscrBdd N is explicitly given by max(1, floor(log((9/4)·N)/log(3·π/4))).

Русский

Если число поле K удовлетворяет условию |дискр K| ≤ N, то его степень над ℚ ограничена величиной rankOfDiscrBdd N, которая равна max(1, ⌊ log((9/4)·N) / log(3π/4) ⌋).

LaTeX

$$$$\\operatorname{finrank}_{\\mathbb{Q}}(K) \\le \\operatorname{rankOfDiscrBdd}(N) = \\max\\{1, \\big\\lfloor \\dfrac{\\log((9/4)N)}{\\log(3\\pi/4)} \\big\\rfloor\\}.$$$$

Lean4

/-- An upper bound on the degree of a number field `K` with `|discr K| ≤ N`,
see `rank_le_rankOfDiscrBdd`. -/
noncomputable abbrev rankOfDiscrBdd : ℕ :=
  max 1 (Nat.floor ((Real.log ((9 / 4 : ℝ) * N) / Real.log (3 * π / 4))))

Похожие утверждения