internlm/Lean-Github huggingface dataset:
Theorem: Ideal.ramificationIdxIn_mul_inertiaDegIn_mul_ncard_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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝ : IsDomain S
this : IsDedekindDomain S
⊢ ramificationIdxIn S p * inertiaDegIn S p * (primesOver S p).ncard = finrank K L
Tactic:
have := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
this : IsFractionRing S L
⊢ ramificationIdxIn S p * inertiaDegIn S p * (primesOver S p).ncard = finrank K L
Theorem: Ideal.ramificationIdxIn_mul_inertiaDegIn_mul_ncard_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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
this : IsFractionRing S L
⊢ ramificationIdxIn S p * inertiaDegIn S p * (primesOver S p).ncard = finrank K L
Tactic:
have := IsIntegralClosure.isNoetherian R K L S
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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : IsNoetherian R S
⊢ ramificationIdxIn S p * inertiaDegIn S p * (primesOver S p).ncard = finrank K L
Theorem: Ideal.ramificationIdxIn_mul_inertiaDegIn_mul_ncard_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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : IsNoetherian R S
⊢ ramificationIdxIn S p * inertiaDegIn S p * (primesOver S p).ncard = finrank K L
Tactic:
have hRS : Function.Injective (algebraMap R S) := by
  refine Function.Injective.of_comp (f := algebraMap S L) ?_
  rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R K L]
  exact (algebraMap K L).injective.comp (IsFractionRing.injective _ _)
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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : IsNoetherian R S
hRS : Function.Injective ⇑(algebraMap R S)
⊢ ramificationIdxIn S p * inertiaDegIn S p * (primesOver S p).ncard = finrank K L
Theorem: Ideal.ramificationIdxIn_mul_inertiaDegIn_mul_ncard_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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : IsNoetherian R S
hRS : Function.Injective ⇑(algebraMap R S)
⊢ ramificationIdxIn S p * inertiaDegIn S p * (primesOver S p).ncard = finrank K L
Tactic:
rw [← NoZeroSMulDivisors.iff_algebraMap_injective] at hRS
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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : IsNoetherian R S
hRS : NoZeroSMulDivisors R S
⊢ ramificationIdxIn S p * inertiaDegIn S p * (primesOver S p).ncard = finrank K L
Theorem: Ideal.ramificationIdxIn_mul_inertiaDegIn_mul_ncard_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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : IsNoetherian R S
hRS : NoZeroSMulDivisors R S
⊢ ramificationIdxIn S p * inertiaDegIn S p * (primesOver S p).ncard = finrank K L
Tactic:
rw [← Ideal.sum_ramification_inertia (S := S) p K L hp, ← coe_primesOverFinset S p hp,
  Set.ncard_coe_Finset, mul_comm, ← smul_eq_mul, ← Finset.sum_const]
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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : IsNoetherian R S
hRS : NoZeroSMulDivisors R S
⊢ ∑ _x ∈ primesOverFinset S p, ramificationIdxIn S p * inertiaDegIn S p =
    ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset,
      ramificationIdx (algebraMap R S) p P * inertiaDeg (algebraMap R S) p P
Theorem: Ideal.ramificationIdxIn_mul_inertiaDegIn_mul_ncard_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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : IsNoetherian R S
hRS : NoZeroSMulDivisors R S
⊢ ∑ _x ∈ primesOverFinset S p, ramificationIdxIn S p * inertiaDegIn S p =
    ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset,
      ramificationIdx (algebraMap R S) p P * inertiaDeg (algebraMap R S) p P
Tactic:
apply Finset.sum_congr 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✝¹ : IsGalois K L
p : Ideal R
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : IsNoetherian R S
hRS : NoZeroSMulDivisors R S
⊢ ∀ x ∈ primesOverFinset S p,
    ramificationIdxIn S p * inertiaDegIn S p = ramificationIdx (algebraMap R S) p x * inertiaDeg (algebraMap R S) p x
Theorem: Ideal.ramificationIdxIn_mul_inertiaDegIn_mul_ncard_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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : IsNoetherian R S
hRS : NoZeroSMulDivisors R S
⊢ ∀ x ∈ primesOverFinset S p,
    ramificationIdxIn S p * inertiaDegIn S p = ramificationIdx (algebraMap R S) p x * inertiaDeg (algebraMap R S) p x
Tactic:
simp_rw [← Finset.mem_coe, coe_primesOverFinset S p hp]
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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : IsNoetherian R S
hRS : NoZeroSMulDivisors R S
⊢ ∀ x ∈ primesOver S p,
    ramificationIdxIn S p * inertiaDegIn S p = ramificationIdx (algebraMap R S) p x * inertiaDeg (algebraMap R S) p x
Theorem: Ideal.ramificationIdxIn_mul_inertiaDegIn_mul_ncard_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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : IsNoetherian R S
hRS : NoZeroSMulDivisors R S
⊢ ∀ x ∈ primesOver S p,
    ramificationIdxIn S p * inertiaDegIn S p = ramificationIdx (algebraMap R S) p x * inertiaDeg (algebraMap R S) p x
Tactic:
intro P hP
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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : IsNoetherian R S
hRS : NoZeroSMulDivisors R S
P : Ideal S
hP : P ∈ primesOver S p
⊢ ramificationIdxIn S p * inertiaDegIn S p = ramificationIdx (algebraMap R S) p P * inertiaDeg (algebraMap R S) p P
Theorem: Ideal.ramificationIdxIn_mul_inertiaDegIn_mul_ncard_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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : IsNoetherian R S
hRS : NoZeroSMulDivisors R S
P : Ideal S
hP : P ∈ primesOver S p
⊢ ramificationIdxIn S p * inertiaDegIn S p = ramificationIdx (algebraMap R S) p P * inertiaDeg (algebraMap R S) p P
Tactic:
rw [Ideal.ramificationIdxIn_eq_ramificationIdx K L p P hP,
  Ideal.inertiaDegIn_eq_inertiaDeg K L p P hP]
Proof state after:
no goals
Theorem: Ideal.ramificationIdxIn_mul_inertiaDegIn_mul_ncard_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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : IsNoetherian R 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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : IsNoetherian R S
⊢ Function.Injective (⇑(algebraMap S L) ∘ ⇑(algebraMap R S))
Theorem: Ideal.ramificationIdxIn_mul_inertiaDegIn_mul_ncard_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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : IsNoetherian R 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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : IsNoetherian R S
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap R K))
Theorem: Ideal.ramificationIdxIn_mul_inertiaDegIn_mul_ncard_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
hp : p ≠ ⊥
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
this✝ : IsFractionRing S L
this : IsNoetherian R 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: ramificationIdxIn_smul_primesOverFinset
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
⊢ Ideal.ramificationIdxIn S p • (primesOverFinset S p).val = factors (Ideal.map (algebraMap R S) p)
Tactic:
have hRS : Function.Injective (algebraMap R S) := by
  refine Function.Injective.of_comp (f := algebraMap S L) ?_
  rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R K L]
  exact (algebraMap K L).injective.comp (IsFractionRing.injective _ _)
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : Function.Injective ⇑(algebraMap R S)
⊢ Ideal.ramificationIdxIn S p • (primesOverFinset S p).val = factors (Ideal.map (algebraMap R S) p)
Theorem: ramificationIdxIn_smul_primesOverFinset
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : Function.Injective ⇑(algebraMap R S)
⊢ Ideal.ramificationIdxIn S p • (primesOverFinset S p).val = factors (Ideal.map (algebraMap R S) p)
Tactic:
rw [← NoZeroSMulDivisors.iff_algebraMap_injective] at hRS
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
⊢ Ideal.ramificationIdxIn S p • (primesOverFinset S p).val = factors (Ideal.map (algebraMap R S) p)
Theorem: ramificationIdxIn_smul_primesOverFinset
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
⊢ Ideal.ramificationIdxIn S p • (primesOverFinset S p).val = factors (Ideal.map (algebraMap R S) p)
Tactic:
by_cases hp : 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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : p = ⊥
⊢ Ideal.ramificationIdxIn S p • (primesOverFinset S p).val = factors (Ideal.map (algebraMap R S) p)

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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
⊢ Ideal.ramificationIdxIn S p • (primesOverFinset S p).val = factors (Ideal.map (algebraMap R S) p)
Theorem: ramificationIdxIn_smul_primesOverFinset
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
⊢ Ideal.ramificationIdxIn S p • (primesOverFinset S p).val = factors (Ideal.map (algebraMap R S) p)
Tactic:
ext P
Proof state after:
case neg.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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
⊢ Multiset.count P (Ideal.ramificationIdxIn S p • (primesOverFinset S p).val) =
    Multiset.count P (factors (Ideal.map (algebraMap R S) p))