can differ from the ring of integers
ProvedGNFS.exists_ringOfIntegers_ne_adjoinalgebraic-number-theorynumber-theory
There exist a monic polynomial , irreducible in , and a complex root of , together with an element such that
- is an algebraic integer, i.e. a root of a monic polynomial with integer coefficients, and
- , the subring of generated by .
So the ring of integers can strictly contain . (A standard example is , .)
Preamble
import Mathlib import Definitions.Def_GNFS_defs open Polynomial IntermediateField
Formal statement
namespace GNFS
theorem exists_ringOfIntegers_ne_adjoin :
∃ (f : ℤ[X]) (θ : ℂ), f.Monic ∧ Irreducible f ∧ aeval θ f = 0 ∧
∃ x : ℂ, x ∈ ℚ⟮θ⟯ ∧ IsIntegral ℤ x ∧ x ∉ Algebra.adjoin ℤ ({θ} : Set ℂ) := by sorry
end GNFSSource
Wikipedia, "General number field sieve" (revision oldid=1377718368, https://en.wikipedia.org/w/index.php?title=General_number_field_sieve&oldid=1377718368), section 'Number fields'
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.