exact IsUnramified.isUnramifiedAt _ hp _ hP
case h.e'_3.h.e'_6
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✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ Ideal.ramificationIdx (algebraMap R S) p P = 1
no goals