letI : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra _ _
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁷ : Field K
inst✝¹⁶ : NumberField K
inst✝¹⁵ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : FiniteDimensional K L
inst✝¹¹ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : finrank K L = ↑p
A : Type u_2
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsIntegralClosure B A L
inst✝ : IsDedekindDomain A
I : Ideal A
hI : Submodule.IsPrincipal (map (algebraMap A B) I)
this✝² : IsDomain B
this✝¹ : IsNoetherian A B
this✝ : IsDedekindDomain B
this : IsFractionRing B L
hAB : NoZeroSMulDivisors A B
⊢ Submodule.IsPrincipal (I ^ finrank K L)
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁷ : Field K
inst✝¹⁶ : NumberField K
inst✝¹⁵ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : FiniteDimensional K L
inst✝¹¹ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : finrank K L = ↑p
A : Type u_2
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsIntegralClosure B A L
inst✝ : IsDedekindDomain A
I : Ideal A
hI : Submodule.IsPrincipal (map (algebraMap A B) I)
this✝³ : IsDomain B
this✝² : IsNoetherian A B
this✝¹ : IsDedekindDomain B
this✝ : IsFractionRing B L
hAB : NoZeroSMulDivisors A B
this : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra A (FractionRing B)
⊢ Submodule.IsPrincipal (I ^ finrank K L)