Theorem: Ideal.inertiaDegIn_bot (FltRegular/NumberTheory/GaloisPrime.lean)

State before:
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
⊢ inertiaDegIn S ⊥ = FiniteDimensional.finrank R S
Tactic:
delta inertiaDegIn
State after:
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
⊢ (if h : (primesOver S ⊥).Nonempty then inertiaDeg (algebraMap R S) ⊥ (Exists.choose h) else 0) =
    FiniteDimensional.finrank R S

State before:
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
⊢ (if h : (primesOver S ⊥).Nonempty then inertiaDeg (algebraMap R S) ⊥ (Exists.choose h) else 0) =
    FiniteDimensional.finrank R S
Tactic:
rw [primesOver_bot]
State after:
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
⊢ (if h : {⊥}.Nonempty then inertiaDeg (algebraMap R S) ⊥ (Exists.choose h) else 0) = FiniteDimensional.finrank R S

State before:
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
⊢ (if h : {⊥}.Nonempty then inertiaDeg (algebraMap R S) ⊥ (Exists.choose h) else 0) = FiniteDimensional.finrank R S
Tactic:
have : ({⊥} : Set (Ideal S)).Nonempty := by simp
State after:
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
⊢ (if h : {⊥}.Nonempty then inertiaDeg (algebraMap R S) ⊥ (Exists.choose h) else 0) = FiniteDimensional.finrank R S

State before:
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
⊢ (if h : {⊥}.Nonempty then inertiaDeg (algebraMap R S) ⊥ (Exists.choose h) else 0) = FiniteDimensional.finrank R S
Tactic:
rw [dif_pos this, this.choose_spec]
State after:
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
⊢ inertiaDeg (algebraMap R S) ⊥ ⊥ = FiniteDimensional.finrank R S

State before:
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
⊢ inertiaDeg (algebraMap R S) ⊥ ⊥ = FiniteDimensional.finrank R S
Tactic:
have hR := not_imp_not.mp (Ring.ne_bot_of_isMaximal_of_not_isField H) rfl
State after:
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

State before:
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
Tactic:
have hS := isField_of_isIntegral_of_isField' (S := S) hR
State after:
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

State before:
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
Tactic:
letI : Field R := hR.toField
State after:
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
this : Field R := hR.toField
⊢ inertiaDeg (algebraMap R S) ⊥ ⊥ = FiniteDimensional.finrank R S

State before:
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
this : Field R := hR.toField
⊢ inertiaDeg (algebraMap R S) ⊥ ⊥ = FiniteDimensional.finrank R S
Tactic:
letI : Field S := hS.toField
State after:
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
this✝ : Field R := hR.toField
this : Field S := hS.toField
⊢ inertiaDeg (algebraMap R S) ⊥ ⊥ = FiniteDimensional.finrank R S

State before:
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
this✝ : Field R := hR.toField
this : Field S := hS.toField
⊢ inertiaDeg (algebraMap R S) ⊥ ⊥ = FiniteDimensional.finrank R S
Tactic:
have : IsIntegralClosure S R S := isIntegralClosure_self
State after:
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
this✝¹ : Field R := hR.toField
this✝ : Field S := hS.toField
this : IsIntegralClosure S R S
⊢ inertiaDeg (algebraMap R S) ⊥ ⊥ = FiniteDimensional.finrank R S

State before:
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
this✝¹ : Field R := hR.toField
this✝ : Field S := hS.toField
this : IsIntegralClosure S R S
⊢ inertiaDeg (algebraMap R S) ⊥ ⊥ = FiniteDimensional.finrank R S
Tactic:
rw [← Ideal.map_bot (f := algebraMap R S), ← finrank_quotient_map (R := R) (S := S) ⊥ R S]
State after:
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
this✝¹ : Field R := hR.toField
this✝ : Field S := hS.toField
this : IsIntegralClosure S R S
⊢ inertiaDeg (algebraMap R S) ⊥ (map (algebraMap R S) ⊥) =
    FiniteDimensional.finrank (R ⧸ ⊥) (S ⧸ map (algebraMap R S) ⊥)

State before:
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
this✝¹ : Field R := hR.toField
this✝ : Field S := hS.toField
this : IsIntegralClosure S R S
⊢ inertiaDeg (algebraMap R S) ⊥ (map (algebraMap R S) ⊥) =
    FiniteDimensional.finrank (R ⧸ ⊥) (S ⧸ map (algebraMap R S) ⊥)
Tactic:
exact inertiaDeg_algebraMap _ _
State after:
no goals

State before:
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
⊢ {⊥}.Nonempty
Tactic:
simp
State after:
no goals