internlm/Lean-Github huggingface dataset:
Theorem: isUnramifiedAt_of_Separable_minpoly'
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✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝⁸ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝⁷ : NoZeroSMulDivisors R S
this✝⁶ : IsNoetherian R S
this✝⁵ : IsDedekindDomain S
this✝⁴ : IsFractionRing S L
this✝³ : (aeval x) (derivative (minpoly R x)) ∈ differentIdeal R S
H✝ :
  (algebraMap (FractionRing R) (FractionRing S)).comp ↑(FractionRing.algEquiv R K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv S L).symm.toRingEquiv).comp (algebraMap K L)
this✝² : IsSeparable (FractionRing R) (FractionRing S)
this✝¹ : p.IsMaximal
P : Ideal S
hP : P ∈ primesOver S p
this✝ : IsScalarTower S (S ⧸ P) (S ⧸ P) := IsScalarTower.right
this : P.IsMaximal
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
⊢ (aeval x) (derivative (minpoly R x)) ∈ P
Tactic:
have : differentIdeal R S ≤ P := by
  rw [← Ideal.dvd_iff_le]
  exact (dvd_pow_self _ H).trans (pow_sub_one_dvd_differentIdeal R S P _ hpbot
  (Ideal.dvd_iff_le.mpr <| Ideal.le_pow_ramificationIdx (p := p) (f := algebraMap R 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✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝⁹ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝⁸ : NoZeroSMulDivisors R S
this✝⁷ : IsNoetherian R S
this✝⁶ : IsDedekindDomain S
this✝⁵ : IsFractionRing S L
this✝⁴ : (aeval x) (derivative (minpoly R x)) ∈ differentIdeal R S
H✝ :
  (algebraMap (FractionRing R) (FractionRing S)).comp ↑(FractionRing.algEquiv R K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv S L).symm.toRingEquiv).comp (algebraMap K L)
this✝³ : IsSeparable (FractionRing R) (FractionRing S)
this✝² : p.IsMaximal
P : Ideal S
hP : P ∈ primesOver S p
this✝¹ : IsScalarTower S (S ⧸ P) (S ⧸ P) := IsScalarTower.right
this✝ : P.IsMaximal
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
this : differentIdeal R S ≤ P
⊢ (aeval x) (derivative (minpoly R x)) ∈ P
Theorem: isUnramifiedAt_of_Separable_minpoly'
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✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝⁹ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝⁸ : NoZeroSMulDivisors R S
this✝⁷ : IsNoetherian R S
this✝⁶ : IsDedekindDomain S
this✝⁵ : IsFractionRing S L
this✝⁴ : (aeval x) (derivative (minpoly R x)) ∈ differentIdeal R S
H✝ :
  (algebraMap (FractionRing R) (FractionRing S)).comp ↑(FractionRing.algEquiv R K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv S L).symm.toRingEquiv).comp (algebraMap K L)
this✝³ : IsSeparable (FractionRing R) (FractionRing S)
this✝² : p.IsMaximal
P : Ideal S
hP : P ∈ primesOver S p
this✝¹ : IsScalarTower S (S ⧸ P) (S ⧸ P) := IsScalarTower.right
this✝ : P.IsMaximal
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
this : differentIdeal R S ≤ P
⊢ (aeval x) (derivative (minpoly R x)) ∈ P
Tactic:
exact this (aeval_derivative_mem_differentIdeal R K L _ hx')
Proof state after:
no goals
Theorem: isUnramifiedAt_of_Separable_minpoly'
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✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝⁸ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝⁷ : NoZeroSMulDivisors R S
this✝⁶ : IsNoetherian R S
this✝⁵ : IsDedekindDomain S
this✝⁴ : IsFractionRing S L
this✝³ : (aeval x) (derivative (minpoly R x)) ∈ differentIdeal R S
H✝ :
  (algebraMap (FractionRing R) (FractionRing S)).comp ↑(FractionRing.algEquiv R K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv S L).symm.toRingEquiv).comp (algebraMap K L)
this✝² : IsSeparable (FractionRing R) (FractionRing S)
this✝¹ : p.IsMaximal
P : Ideal S
hP : P ∈ primesOver S p
this✝ : IsScalarTower S (S ⧸ P) (S ⧸ P) := IsScalarTower.right
this : P.IsMaximal
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
⊢ differentIdeal R S ≤ P
Tactic:
rw [← Ideal.dvd_iff_le]
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✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝⁸ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝⁷ : NoZeroSMulDivisors R S
this✝⁶ : IsNoetherian R S
this✝⁵ : IsDedekindDomain S
this✝⁴ : IsFractionRing S L
this✝³ : (aeval x) (derivative (minpoly R x)) ∈ differentIdeal R S
H✝ :
  (algebraMap (FractionRing R) (FractionRing S)).comp ↑(FractionRing.algEquiv R K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv S L).symm.toRingEquiv).comp (algebraMap K L)
this✝² : IsSeparable (FractionRing R) (FractionRing S)
this✝¹ : p.IsMaximal
P : Ideal S
hP : P ∈ primesOver S p
this✝ : IsScalarTower S (S ⧸ P) (S ⧸ P) := IsScalarTower.right
this : P.IsMaximal
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
⊢ P ∣ differentIdeal R S
Theorem: isUnramifiedAt_of_Separable_minpoly'
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✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝⁸ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝⁷ : NoZeroSMulDivisors R S
this✝⁶ : IsNoetherian R S
this✝⁵ : IsDedekindDomain S
this✝⁴ : IsFractionRing S L
this✝³ : (aeval x) (derivative (minpoly R x)) ∈ differentIdeal R S
H✝ :
  (algebraMap (FractionRing R) (FractionRing S)).comp ↑(FractionRing.algEquiv R K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv S L).symm.toRingEquiv).comp (algebraMap K L)
this✝² : IsSeparable (FractionRing R) (FractionRing S)
this✝¹ : p.IsMaximal
P : Ideal S
hP : P ∈ primesOver S p
this✝ : IsScalarTower S (S ⧸ P) (S ⧸ P) := IsScalarTower.right
this : P.IsMaximal
H : ¬Ideal.ramificationIdx (algebraMap R S) p P - 1 = 0
⊢ P ∣ differentIdeal R S
Tactic:
exact (dvd_pow_self _ H).trans (pow_sub_one_dvd_differentIdeal R S P _ hpbot
(Ideal.dvd_iff_le.mpr <| Ideal.le_pow_ramificationIdx (p := p) (f := algebraMap R S)))
Proof state after:
no goals
Theorem: isUnramifiedAt_of_Separable_minpoly'
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✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝⁸ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝⁷ : NoZeroSMulDivisors R S
this✝⁶ : IsNoetherian R S
this✝⁵ : IsDedekindDomain S
this✝⁴ : IsFractionRing S L
this✝³ : (aeval x) (derivative (minpoly R x)) ∈ differentIdeal R S
H :
  (algebraMap (FractionRing R) (FractionRing S)).comp ↑(FractionRing.algEquiv R K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv S L).symm.toRingEquiv).comp (algebraMap K L)
this✝² : IsSeparable (FractionRing R) (FractionRing S)
this✝¹ : p.IsMaximal
P : Ideal S
hP : P ∈ primesOver S p
this✝ : IsScalarTower S (S ⧸ P) (S ⧸ P) := IsScalarTower.right
this : P.IsMaximal
⊢ 1 ≤ Ideal.ramificationIdx (algebraMap R S) p P
Tactic:
rwa [Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count _
  (isMaximal_of_mem_primesOver hpbot hP).isPrime (ne_bot_of_mem_primesOver hpbot hP),
  Multiset.one_le_count_iff_mem, ← Multiset.mem_toFinset, ← primesOverFinset,
  ← Finset.mem_coe, coe_primesOverFinset _ p hpbot]
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✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝⁸ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝⁷ : NoZeroSMulDivisors R S
this✝⁶ : IsNoetherian R S
this✝⁵ : IsDedekindDomain S
this✝⁴ : IsFractionRing S L
this✝³ : (aeval x) (derivative (minpoly R x)) ∈ differentIdeal R S
H :
  (algebraMap (FractionRing R) (FractionRing S)).comp ↑(FractionRing.algEquiv R K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv S L).symm.toRingEquiv).comp (algebraMap K L)
this✝² : IsSeparable (FractionRing R) (FractionRing S)
this✝¹ : p.IsMaximal
P : Ideal S
hP : P ∈ primesOver S p
this✝ : IsScalarTower S (S ⧸ P) (S ⧸ P) := IsScalarTower.right
this : P.IsMaximal
⊢ Ideal.map (algebraMap R S) p ≠ ⊥
Theorem: isUnramifiedAt_of_Separable_minpoly'
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✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : S
hx' : Algebra.adjoin K {(algebraMap S L) x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
this✝⁸ : IsDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝⁷ : NoZeroSMulDivisors R S
this✝⁶ : IsNoetherian R S
this✝⁵ : IsDedekindDomain S
this✝⁴ : IsFractionRing S L
this✝³ : (aeval x) (derivative (minpoly R x)) ∈ differentIdeal R S
H :
  (algebraMap (FractionRing R) (FractionRing S)).comp ↑(FractionRing.algEquiv R K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv S L).symm.toRingEquiv).comp (algebraMap K L)
this✝² : IsSeparable (FractionRing R) (FractionRing S)
this✝¹ : p.IsMaximal
P : Ideal S
hP : P ∈ primesOver S p
this✝ : IsScalarTower S (S ⧸ P) (S ⧸ P) := IsScalarTower.right
this : P.IsMaximal
⊢ Ideal.map (algebraMap R S) p ≠ ⊥
Tactic:
rwa [ne_eq, Ideal.map_eq_bot_iff_of_injective hRS]
Proof state after:
no goals
Theorem: isUnramifiedAt_of_Separable_minpoly
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✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : L
hx : IsIntegral R x
hx' : Algebra.adjoin K {x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R x)).Separable
⊢ IsUnramifiedAt S p
Tactic:
rw [← IsIntegralClosure.algebraMap_mk' S x hx, minpoly.algebraMap_eq
  (IsIntegralClosure.algebraMap_injective S R L)] at h
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✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : L
hx : IsIntegral R x
hx' : Algebra.adjoin K {x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R (IsIntegralClosure.mk' S x hx))).Separable
⊢ IsUnramifiedAt S p
Theorem: isUnramifiedAt_of_Separable_minpoly
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✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : L
hx : IsIntegral R x
hx' : Algebra.adjoin K {x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R (IsIntegralClosure.mk' S x hx))).Separable
⊢ IsUnramifiedAt S p
Tactic:
exact isUnramifiedAt_of_Separable_minpoly' K L p hpbot (IsIntegralClosure.mk' S x hx)
  (by rwa [IsIntegralClosure.algebraMap_mk']) h
Proof state after:
no goals
Theorem: isUnramifiedAt_of_Separable_minpoly
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✝ : IsSeparable K L
p : Ideal R
hp : p.IsPrime
hpbot : p ≠ ⊥
x : L
hx : IsIntegral R x
hx' : Algebra.adjoin K {x} = ⊤
h : (map (Ideal.Quotient.mk p) (minpoly R (IsIntegralClosure.mk' S x hx))).Separable
⊢ Algebra.adjoin K {(algebraMap S L) (IsIntegralClosure.mk' S x hx)} = ⊤
Tactic:
rwa [IsIntegralClosure.algebraMap_mk']
Proof state after:
no goals
Theorem: IsPrimitiveRoot.unit'_pow
Proof state before:
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ hζ.unit' ^ ↑p = 1
Tactic:
ext
Proof state after:
case a.h
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ ↑↑(hζ.unit' ^ ↑p) = ↑↑1
Theorem: IsPrimitiveRoot.unit'_pow
Proof state before:
case a.h
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ ↑↑(hζ.unit' ^ ↑p) = ↑↑1
Tactic:
simpa using hζ.pow_eq_one
Proof state after:
no goals
Theorem: zeta_runity_pow_even
Proof state before:
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hpo : Odd ↑p
n : ℕ
⊢ ∃ m, hζ.unit' ^ n = hζ.unit' ^ (2 * m)
Tactic:
rcases eq_or_ne n 0 with (rfl | _)
Proof state after:
case inl
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hpo : Odd ↑p
⊢ ∃ m, hζ.unit' ^ 0 = hζ.unit' ^ (2 * m)

case inr
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hpo : Odd ↑p
n : ℕ
h✝ : n ≠ 0
⊢ ∃ m, hζ.unit' ^ n = hζ.unit' ^ (2 * m)
Theorem: zeta_runity_pow_even
Proof state before:
case inr
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hpo : Odd ↑p
n : ℕ
h✝ : n ≠ 0
⊢ ∃ m, hζ.unit' ^ n = hζ.unit' ^ (2 * m)
Tactic:
obtain ⟨r, hr⟩ := hpo
Proof state after:
case inr.intro
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
⊢ ∃ m, hζ.unit' ^ n = hζ.unit' ^ (2 * m)
Theorem: zeta_runity_pow_even
Proof state before:
case inr.intro
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
⊢ ∃ m, hζ.unit' ^ n = hζ.unit' ^ (2 * m)
Tactic:
have he : 2 * (r + 1) * n = p * n + n := by rw [hr]; ring
Proof state after:
case inr.intro
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
he : 2 * (r + 1) * n = ↑p * n + n
⊢ ∃ m, hζ.unit' ^ n = hζ.unit' ^ (2 * m)
Theorem: zeta_runity_pow_even
Proof state before:
case inr.intro
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
he : 2 * (r + 1) * n = ↑p * n + n
⊢ ∃ m, hζ.unit' ^ n = hζ.unit' ^ (2 * m)
Tactic:
use (r + 1) * n
Proof state after:
case h
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
he : 2 * (r + 1) * n = ↑p * n + n
⊢ hζ.unit' ^ n = hζ.unit' ^ (2 * ((r + 1) * n))
Theorem: zeta_runity_pow_even
Proof state before:
case h
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
he : 2 * (r + 1) * n = ↑p * n + n
⊢ hζ.unit' ^ n = hζ.unit' ^ (2 * ((r + 1) * n))
Tactic:
rw [← mul_assoc, he, pow_add]
Proof state after:
case h
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
he : 2 * (r + 1) * n = ↑p * n + n
⊢ hζ.unit' ^ n = hζ.unit' ^ (↑p * n) * hζ.unit' ^ n
Theorem: zeta_runity_pow_even
Proof state before:
case h
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
he : 2 * (r + 1) * n = ↑p * n + n
⊢ hζ.unit' ^ n = hζ.unit' ^ (↑p * n) * hζ.unit' ^ n
Tactic:
convert (one_mul (M := (𝓞 K)ˣ) _).symm
Proof state after:
case h.e'_3.h.e'_5
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
he : 2 * (r + 1) * n = ↑p * n + n
⊢ hζ.unit' ^ (↑p * n) = 1
Theorem: zeta_runity_pow_even
Proof state before:
case h.e'_3.h.e'_5
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
he : 2 * (r + 1) * n = ↑p * n + n
⊢ hζ.unit' ^ (↑p * n) = 1
Tactic:
rw [pow_mul, hζ.unit'_pow, one_pow]
Proof state after:
no goals
Theorem: zeta_runity_pow_even
Proof state before:
case inl
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hpo : Odd ↑p
⊢ ∃ m, hζ.unit' ^ 0 = hζ.unit' ^ (2 * m)
Tactic:
use 0
Proof state after:
no goals
Theorem: zeta_runity_pow_even
Proof state before:
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
⊢ 2 * (r + 1) * n = ↑p * n + n
Tactic:
rw [hr]
Proof state after:
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
⊢ 2 * (r + 1) * n = (2 * r + 1) * n + n
Theorem: zeta_runity_pow_even
Proof state before:
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
⊢ 2 * (r + 1) * n = (2 * r + 1) * n + n
Tactic:
ring
Proof state after:
no goals
Theorem: IsPrimitiveRoot.unit'_coe
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
⊢ IsPrimitiveRoot ↑hζ.unit' ↑p
Tactic:
have z1 := hζ
Proof state after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
z1 : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot ↑hζ.unit' ↑p
Theorem: IsPrimitiveRoot.unit'_coe
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
z1 : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot ↑hζ.unit' ↑p
Tactic:
have : (algebraMap R K) (hζ.unit' : R) = ζ := rfl
Proof state after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
z1 : IsPrimitiveRoot ζ ↑p
this : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
⊢ IsPrimitiveRoot ↑hζ.unit' ↑p
Theorem: IsPrimitiveRoot.unit'_coe
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
z1 : IsPrimitiveRoot ζ ↑p
this : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
⊢ IsPrimitiveRoot ↑hζ.unit' ↑p
Tactic:
rw [← this] at z1
Proof state after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
z1 : IsPrimitiveRoot ((algebraMap (𝓞 K) K) ↑hζ.unit') ↑p
this : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
⊢ IsPrimitiveRoot ↑hζ.unit' ↑p
Theorem: IsPrimitiveRoot.unit'_coe
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
z1 : IsPrimitiveRoot ((algebraMap (𝓞 K) K) ↑hζ.unit') ↑p
this : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
⊢ IsPrimitiveRoot ↑hζ.unit' ↑p
Tactic:
exact z1.of_map_of_injective (IsFractionRing.injective _ _)
Proof state after:
no goals
Theorem: contains_two_primitive_roots
Proof state before:
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
rcases Nat.eq_zero_or_pos p with (rfl | hppos)
Proof state after:
case inl
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hy : IsPrimitiveRoot y q
hx : IsPrimitiveRoot x 0
⊢ (lcm 0 q).totient ≤ FiniteDimensional.finrank ℚ K

case inr
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Theorem: contains_two_primitive_roots
Proof state before:
case inr
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K
Tactic:
rcases Nat.eq_zero_or_pos q with (rfl | hqpos)
Proof state after:
case inr.inl
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hppos : p > 0
hy : IsPrimitiveRoot y 0
⊢ (lcm p 0).totient ≤ FiniteDimensional.finrank ℚ K

case inr.inr
p✝ : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
inst✝¹ : NumberField K
p q : ℕ
x y : K
inst✝ : FiniteDimensional ℚ K
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
⊢ (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K