A primitive integral generator has nonzero conductor exponent

The discriminant of its rational power basis clears denominators in the ring of integers. Thus the excluded conductor primes form a finite set.

theorem NairTenenbaum.ringOfIntegers_mem_adjoin_iff {K : Type u_1} [Field K] (θ x : NumberField.RingOfIntegers K) : ↑x ∈ ℤ[↑θ] ↔ x ∈ ℤ[θ]

theorem NairTenenbaum.exists_nonzero_integer_mem_conductor {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) (B : PowerBasis ℚ K) (hB : B.gen = ↑θ) : ∃ (d : ℤ), d ≠ 0 ∧ ↑d ∈ conductor ℤ θ

theorem NairTenenbaum.conductor_exponent_ne_zero {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) (B : PowerBasis ℚ K) (hB : B.gen = ↑θ) : RingOfIntegers.exponent θ ≠ 0