discr — Mathlib

English

If |discr K| ≤ N, then natDegree of minpoly over ℤ of an integral element a is bounded by rankOfDiscrBdd N.

Русский

Если |дискр K| ≤ N, то натуральная степень минимального многочлена над ℤ элемента a ограничена rankOfDiscrBdd N.

LaTeX

$$$$\\operatorname{natDegree}(\\minpoly_{\\mathbb{Z}}(a)) \\le \\operatorname{rankOfDiscrBdd}(N).$$$$

Lean4

/-- The absolute discriminant of a number field. -/
noncomputable abbrev discr : ℤ :=
  Algebra.discr ℤ (RingOfIntegers.basis K)

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