exact PowerBasis.isIntegral_gen pb
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : NoZeroSMulDivisors R S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra.IsIntegral R S
pb : PowerBasis R S
p : Ideal R
inst✝ : p.IsPrime
hpbot : p ≠ ⊥
⊢ IsIntegral R pb.gen
no goals