have hS := isField_of_isIntegral_of_isField' (S := S) hR
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✝⁴ : Nontrivial R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsNoetherian R S
inst✝ : Algebra.IsIntegral R S
H : ⊥.IsMaximal
this : {⊥}.Nonempty
hR : IsField R
⊢ inertiaDeg (algebraMap R S) ⊥ ⊥ = FiniteDimensional.finrank R S
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✝⁴ : Nontrivial R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : IsNoetherian R S
inst✝ : Algebra.IsIntegral R S
H : ⊥.IsMaximal
this : {⊥}.Nonempty
hR : IsField R
hS : IsField S
⊢ inertiaDeg (algebraMap R S) ⊥ ⊥ = FiniteDimensional.finrank R S