have hRS : Algebra.IsIntegral R S := IsIntegralClosure.isIntegral_algebra R L
case pos
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✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
this : ↑P ∈ primesOver S ⊥
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) ⊥ ^ Ideal.inertiaDegIn S ⊥
case pos
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✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS✝ : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
this : ↑P ∈ primesOver S ⊥
hRS : Algebra.IsIntegral R S
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) ⊥ ^ Ideal.inertiaDegIn S ⊥