internlm/Lean-Github huggingface dataset:
Theorem: primesOver_nonempty
Proof state before:
R : Type u_2
S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsIntegral R S
p : Ideal R
inst✝ : p.IsPrime
this : ⊥.IsPrime
⊢ ⊥ ≤ p
Tactic:
exact bot_le
Proof state after:
no goals
Theorem: ne_bot_of_mem_primesOver
Proof state before:
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
hP' : P = ⊥
⊢ p = ⊥
Tactic:
rw [← hP.2, hP', ← RingHom.ker_eq_comap_bot, ← RingHom.injective_iff_ker_eq_bot]
Proof state after:
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
hP' : P = ⊥
⊢ Function.Injective ⇑(algebraMap R S)
Theorem: ne_bot_of_mem_primesOver
Proof state before:
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
hP' : P = ⊥
⊢ Function.Injective ⇑(algebraMap R S)
Tactic:
exact NoZeroSMulDivisors.algebraMap_injective R S
Proof state after:
no goals
Theorem: prod_galRestrictHom_eq_norm
Proof 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✝ : IsGalois K L
x : S
⊢ ∏ σ : L ≃ₐ[K] L, ((galRestrictHom R K L S) ↑σ) x =
    (algebraMap R S) (IsIntegralClosure.mk' R ((Algebra.norm K) ((algebraMap S L) x)) ⋯)
Tactic:
apply IsIntegralClosure.algebraMap_injective S R L
Proof state after:
case a
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
x : S
⊢ (algebraMap S L) (∏ σ : L ≃ₐ[K] L, ((galRestrictHom R K L S) ↑σ) x) =
    (algebraMap S L) ((algebraMap R S) (IsIntegralClosure.mk' R ((Algebra.norm K) ((algebraMap S L) x)) ⋯))
Theorem: prod_galRestrictHom_eq_norm
Proof state before:
case a
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
x : S
⊢ (algebraMap S L) (∏ σ : L ≃ₐ[K] L, ((galRestrictHom R K L S) ↑σ) x) =
    (algebraMap S L) ((algebraMap R S) (IsIntegralClosure.mk' R ((Algebra.norm K) ((algebraMap S L) x)) ⋯))
Tactic:
rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_eq R K L]
Proof state after:
case a
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
x : S
⊢ (algebraMap S L) (∏ σ : L ≃ₐ[K] L, ((galRestrictHom R K L S) ↑σ) x) =
    ((algebraMap K L).comp (algebraMap R K)) (IsIntegralClosure.mk' R ((Algebra.norm K) ((algebraMap S L) x)) ⋯)
Theorem: prod_galRestrictHom_eq_norm
Proof state before:
case a
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
x : S
⊢ (algebraMap S L) (∏ σ : L ≃ₐ[K] L, ((galRestrictHom R K L S) ↑σ) x) =
    ((algebraMap K L).comp (algebraMap R K)) (IsIntegralClosure.mk' R ((Algebra.norm K) ((algebraMap S L) x)) ⋯)
Tactic:
simp only [map_prod, algebraMap_galRestrictHom_apply, IsIntegralClosure.algebraMap_mk',
  Algebra.norm_eq_prod_automorphisms, AlgHom.coe_coe, RingHom.coe_comp, Function.comp_apply]
Proof state after:
no goals
Theorem: Ideal.ramificationIdxIn_bot
Proof 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
⊢ ramificationIdxIn S ⊥ = 0
Tactic:
delta ramificationIdxIn
Proof 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
⊢ (if h : (primesOver S ⊥).Nonempty then ramificationIdx (algebraMap R S) ⊥ (Exists.choose h) else 0) = 0
Theorem: Ideal.ramificationIdxIn_bot
Proof 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
⊢ (if h : (primesOver S ⊥).Nonempty then ramificationIdx (algebraMap R S) ⊥ (Exists.choose h) else 0) = 0
Tactic:
by_cases h : (primesOver S (⊥ : Ideal R)).Nonempty
Proof state after:
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
h : (primesOver S ⊥).Nonempty
⊢ (if h : (primesOver S ⊥).Nonempty then ramificationIdx (algebraMap R S) ⊥ (Exists.choose h) else 0) = 0

case neg
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
h : ¬(primesOver S ⊥).Nonempty
⊢ (if h : (primesOver S ⊥).Nonempty then ramificationIdx (algebraMap R S) ⊥ (Exists.choose h) else 0) = 0
Theorem: Ideal.ramificationIdxIn_bot
Proof state before:
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
h : (primesOver S ⊥).Nonempty
⊢ (if h : (primesOver S ⊥).Nonempty then ramificationIdx (algebraMap R S) ⊥ (Exists.choose h) else 0) = 0
Tactic:
rw [dif_pos h, ramificationIdx_bot]
Proof state after:
no goals
Theorem: Ideal.ramificationIdxIn_bot
Proof state before:
case neg
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
h : ¬(primesOver S ⊥).Nonempty
⊢ (if h : (primesOver S ⊥).Nonempty then ramificationIdx (algebraMap R S) ⊥ (Exists.choose h) else 0) = 0
Tactic:
exact dif_neg h
Proof state after:
no goals
Theorem: Ideal.inertiaDegIn_bot
Proof 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
Proof 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
Theorem: Ideal.inertiaDegIn_bot
Proof 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]
Proof 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
Theorem: Ideal.inertiaDegIn_bot
Proof 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
Proof 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
Theorem: Ideal.inertiaDegIn_bot
Proof 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]
Proof 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
Theorem: Ideal.inertiaDegIn_bot
Proof 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
Proof 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
Theorem: Ideal.inertiaDegIn_bot
Proof 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
Proof 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
Theorem: Ideal.inertiaDegIn_bot
Proof 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
Proof 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
Theorem: Ideal.inertiaDegIn_bot
Proof 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
Proof 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
Theorem: Ideal.inertiaDegIn_bot
Proof 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
Proof 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