internlm/Lean-Github huggingface dataset:
Theorem: prod_smul_primesOver
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
inst✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
⊢ (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val).prod =
    ((Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p) • (primesOverFinset S p).val).prod
Tactic:
congr
Proof state after:
case neg.e_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
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
⊢ Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val =
    (Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p) • (primesOverFinset S p).val
Theorem: prod_smul_primesOver
Proof state before:
case neg.e_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
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
⊢ Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val =
    (Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p) • (primesOverFinset S p).val
Tactic:
ext P'
Proof state after:
case neg.e_a.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
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Multiset.count P' ((Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p) • (primesOverFinset S p).val)
Theorem: prod_smul_primesOver
Proof state before:
case neg.e_a.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
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Multiset.count P' ((Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p) • (primesOverFinset S p).val)
Tactic:
rw [Multiset.count_nsmul, primesOverFinset, Multiset.toFinset_val, Multiset.count_dedup]
Proof state after:
case neg.e_a.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
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * if P' ∈ factors (Ideal.map (algebraMap R S) p) then 1 else 0
Theorem: prod_smul_primesOver
Proof state before:
case neg.e_a.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
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * if P' ∈ factors (Ideal.map (algebraMap R S) p) then 1 else 0
Tactic:
simp_rw [← Multiset.mem_toFinset, ← Finset.mem_coe]
Proof state after:
case neg.e_a.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
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p *
      if P' ∈ ↑(factors (Ideal.map (algebraMap R S) p)).toFinset then 1 else 0
Theorem: prod_smul_primesOver
Proof state before:
case neg.e_a.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
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p *
      if P' ∈ ↑(factors (Ideal.map (algebraMap R S) p)).toFinset then 1 else 0
Tactic:
rw [← primesOverFinset]
Proof state after:
case neg.e_a.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
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * if P' ∈ ↑(primesOverFinset S p) then 1 else 0
Theorem: prod_smul_primesOver
Proof state before:
case neg.e_a.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
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * if P' ∈ ↑(primesOverFinset S p) then 1 else 0
Tactic:
simp_rw [coe_primesOverFinset S p hp]
Proof state after:
case neg.e_a.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
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * if P' ∈ primesOver S p then 1 else 0
Theorem: prod_smul_primesOver
Proof state before:
case neg.e_a.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
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * if P' ∈ primesOver S p then 1 else 0
Tactic:
by_cases hP' : P' ∈ primesOver S p
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
inst✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * if P' ∈ primesOver S p then 1 else 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
inst✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∉ primesOver S p
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * if P' ∈ primesOver S p then 1 else 0
Theorem: prod_smul_primesOver
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
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝ : IsDomain S
this : IsDedekindDomain S
⊢ Function.Injective ⇑(algebraMap R S)
Tactic:
refine Function.Injective.of_comp (f := algebraMap S L) ?_
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝ : IsDomain S
this : IsDedekindDomain S
⊢ Function.Injective (⇑(algebraMap S L) ∘ ⇑(algebraMap R S))
Theorem: prod_smul_primesOver
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
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝ : IsDomain S
this : IsDedekindDomain S
⊢ Function.Injective (⇑(algebraMap S L) ∘ ⇑(algebraMap R S))
Tactic:
rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R K L]
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝ : IsDomain S
this : IsDedekindDomain S
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap R K))
Theorem: prod_smul_primesOver
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
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝ : IsDomain S
this : IsDedekindDomain S
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap R K))
Tactic:
exact (algebraMap K L).injective.comp (IsFractionRing.injective _ _)
Proof state after:
no goals
Theorem: prod_smul_primesOver
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
inst✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : p = ⊥
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) p ^ Ideal.inertiaDegIn S p
Tactic:
subst hp
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
inst✝¹ : IsGalois K L
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) ⊥ ^ Ideal.inertiaDegIn S ⊥
Theorem: prod_smul_primesOver
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
inst✝¹ : IsGalois K L
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) ⊥ ^ Ideal.inertiaDegIn S ⊥
Tactic:
have := P.prop
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
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 ⊥
Theorem: prod_smul_primesOver
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
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 ⊥
Tactic:
have hRS : Algebra.IsIntegral R S := IsIntegralClosure.isIntegral_algebra R L
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
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 ⊥
Theorem: prod_smul_primesOver
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
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 ⊥
Tactic:
simp_rw [primesOver_bot (S := S),
  Set.mem_singleton_iff] at this
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
inst✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS✝ : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
hRS : Algebra.IsIntegral R S
this : ↑P = ⊥
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) ⊥ ^ Ideal.inertiaDegIn S ⊥
Theorem: prod_smul_primesOver
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
inst✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS✝ : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
hRS : Algebra.IsIntegral R S
this : ↑P = ⊥
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) ⊥ ^ Ideal.inertiaDegIn S ⊥
Tactic:
simp_rw [coe_smul_primesOver, this,
  Ideal.comap_bot_of_injective _ (galRestrict R K L S _).injective, Finset.prod_const,
  Ideal.map_bot, Ideal.inertiaDegIn_bot R S]
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
inst✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS✝ : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
hRS : Algebra.IsIntegral R S
this : ↑P = ⊥
⊢ ⊥ ^ Finset.univ.card = ⊥ ^ finrank R S