apply IsPrincipal_of_IsPrincipal_pow_of_Coprime (𝓞 K') _ hreg I
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
⊢ Submodule.IsPrincipal I
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
⊢ Submodule.IsPrincipal (I ^ p)