show Submodule.IsPrincipal (Izero.unit' : FractionalIdeal A⁰ K)
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ (↑I).IsPrincipal
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ (↑↑Izero.unit').IsPrincipal