for irreducible
ProvedGNFS.finrank_adjoin_root_eq_natDegreealgebraic-number-theorynumber-theory
Let be irreducible of degree , and let satisfy . Then the subfield generated by has dimension as a vector space over :
So every element of is written uniquely as with , which is how GNFS represents number-field elements.
Preamble
import Mathlib import Definitions.Def_GNFS_defs open Polynomial IntermediateField
Formal statement
namespace GNFS
theorem finrank_adjoin_root_eq_natDegree (f : ℚ[X]) (hf : Irreducible f) (θ : ℂ)
(hθ : aeval θ f = 0) :
Module.finrank ℚ ℚ⟮θ⟯ = f.natDegree := 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.