rwa [Ideal.absNorm_span_singleton, ← Int.prime_iff_natAbs_prime]
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
inst✝² : Infinite R
inst✝¹ : Module.Free ℤ R
inst✝ : Module.Finite ℤ R
x : R
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ (Ideal.absNorm (Ideal.span {x})).Prime
no goals