Units of a number field of prime degree

In a number field of prime degree, a non-torsion unit lies in no proper subfield, since a unit with rational value is torsion, and therefore generates K over ℚ. This is what lets a statement about integral primitive elements of K apply to every non-torsion unit when the degree is prime.

Main results

• TauCeti.NumberField.Units.adjoin_eq_top_of_finrank_prime: in prime degree, a non-torsion unit generates K over ℚ.

theorem TauCeti.NumberField.Units.adjoin_eq_top_of_finrank_prime {K : Type u_1} [Field K] [NumberField K] (hp : Nat.Prime (Module.finrank ℚ K)) {v : (NumberField.RingOfIntegers K)ˣ} (hv : v ∉ NumberField.Units.torsion K) : ℚ[↑↑v] = ⊤

Prime degree makes a competing unit a generator. In a number field of prime degree, a non-torsion unit generates K over ℚ.