infer_instance
case h.e'_2
n p : ℕ
inst✝⁷ : Fact p.Prime
A : Type ?u.39073
K : Type ?u.39076
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
L : Type ?u.39509
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ IsPrincipalIdealRing (𝓞 (CyclotomicField ⟨2, ⋯⟩ ℚ))
no goals