internlm/Lean-Github huggingface dataset:
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
⊢ IsPrimitiveRoot x l
Tactic:
have : (algebraMap R K) ⟨x, hx⟩ = x := by rfl
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
this : (algebraMap (𝓞 K) K) ⟨x, hx⟩ = x
⊢ IsPrimitiveRoot x l
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
this : (algebraMap (𝓞 K) K) ⟨x, hx⟩ = x
⊢ IsPrimitiveRoot x l
Tactic:
have h4 := IsPrimitiveRoot.map_of_injective hpl' (f := algebraMap (𝓞 K) K)
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
this : (algebraMap (𝓞 K) K) ⟨x, hx⟩ = x
h4 : Function.Injective ⇑(algebraMap (𝓞 K) K) → IsPrimitiveRoot ((algebraMap (𝓞 K) K) ⟨x, hx⟩) l
⊢ IsPrimitiveRoot x l
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
this : (algebraMap (𝓞 K) K) ⟨x, hx⟩ = x
h4 : Function.Injective ⇑(algebraMap (𝓞 K) K) → IsPrimitiveRoot ((algebraMap (𝓞 K) K) ⟨x, hx⟩) l
⊢ IsPrimitiveRoot x l
Tactic:
rw [← this]
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
this : (algebraMap (𝓞 K) K) ⟨x, hx⟩ = x
h4 : Function.Injective ⇑(algebraMap (𝓞 K) K) → IsPrimitiveRoot ((algebraMap (𝓞 K) K) ⟨x, hx⟩) l
⊢ IsPrimitiveRoot ((algebraMap (𝓞 K) K) ⟨x, hx⟩) l
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
this : (algebraMap (𝓞 K) K) ⟨x, hx⟩ = x
h4 : Function.Injective ⇑(algebraMap (𝓞 K) K) → IsPrimitiveRoot ((algebraMap (𝓞 K) K) ⟨x, hx⟩) l
⊢ IsPrimitiveRoot ((algebraMap (𝓞 K) K) ⟨x, hx⟩) l
Tactic:
apply h4
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
this : (algebraMap (𝓞 K) K) ⟨x, hx⟩ = x
h4 : Function.Injective ⇑(algebraMap (𝓞 K) K) → IsPrimitiveRoot ((algebraMap (𝓞 K) K) ⟨x, hx⟩) l
⊢ Function.Injective ⇑(algebraMap (𝓞 K) K)
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
this : (algebraMap (𝓞 K) K) ⟨x, hx⟩ = x
h4 : Function.Injective ⇑(algebraMap (𝓞 K) K) → IsPrimitiveRoot ((algebraMap (𝓞 K) K) ⟨x, hx⟩) l
⊢ Function.Injective ⇑(algebraMap (𝓞 K) K)
Tactic:
apply IsFractionRing.injective
Proof state after:
no goals
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
⊢ (algebraMap (𝓞 K) K) ⟨x, hx⟩ = x
Tactic:
rfl
Proof state after:
no goals
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
pdivlcm_h : lcm l ↑p = ↑p * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
⊢ 0 < pdivlcm_w
Tactic:
by_contra h
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h✝ : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
pdivlcm_h : lcm l ↑p = ↑p * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
h : ¬0 < pdivlcm_w
⊢ False
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h✝ : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
pdivlcm_h : lcm l ↑p = ↑p * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
h : ¬0 < pdivlcm_w
⊢ False
Tactic:
simp only [not_lt, le_zero_iff] at h
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h✝ : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
pdivlcm_h : lcm l ↑p = ↑p * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
h : pdivlcm_w = 0
⊢ False
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h✝ : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
pdivlcm_h : lcm l ↑p = ↑p * pdivlcm_w
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
h : pdivlcm_w = 0
⊢ False
Tactic:
rw [h] at pdivlcm_h
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h✝ : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
pdivlcm_h : lcm l ↑p = ↑p * 0
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
h : pdivlcm_w = 0
⊢ False
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h✝ : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
pdivlcm_h : lcm l ↑p = ↑p * 0
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
h : pdivlcm_w = 0
⊢ False
Tactic:
simp only [MulZeroClass.mul_zero, lcm_eq_zero_iff, PNat.ne_zero, or_false_iff] at pdivlcm_h
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h✝ : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
h : pdivlcm_w = 0
pdivlcm_h : l = 0
⊢ False
Theorem: roots_of_unity_in_cyclo_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
x : K
n l : ℕ
hl : l ∈ n.divisors
hx : IsIntegral ℤ x
hhl : (cyclotomic l (𝓞 K)).IsRoot ⟨x, hx⟩
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
h✝ : ¬l ∣ 2 * ↑p
hpl' : IsPrimitiveRoot ⟨x, hx⟩ l
hpl : IsPrimitiveRoot x l
KEY : (lcm l ↑p).totient ≤ (↑p).totient
hirr : Irreducible (cyclotomic ↑p ℚ)
hrank : FiniteDimensional.finrank ℚ K = (↑p).totient
pdivlcm_w : ℕ
ineq1 : (↑p).totient * pdivlcm_w.totient ≤ (lcm l ↑p).totient
KEY3 : pdivlcm_w.totient ≤ 1
h : pdivlcm_w = 0
pdivlcm_h : l = 0
⊢ False
Tactic:
apply absurd pdivlcm_h (ne_of_gt (Nat.pos_of_mem_divisors hl))
Proof state after:
no goals
Theorem: roots_of_unity_in_cyclo
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
h : ∃ n, ∃ (_ : 0 < n), x ^ n = 1
⊢ ∃ m k, x = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Tactic:
obtain ⟨n, hn0, hn⟩ := h
Proof state after:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
⊢ ∃ m k, x = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Theorem: roots_of_unity_in_cyclo
Proof state before:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
⊢ ∃ m k, x = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Tactic:
have hxu : (⟨x, hx⟩ : R) ^ n = 1 := by ext; simp [hn]
Proof state after:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
⊢ ∃ m k, x = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Theorem: roots_of_unity_in_cyclo
Proof state before:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
H : ∃ m k, ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
⊢ ∃ m k, x = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Tactic:
obtain ⟨m, k, hmk⟩ := H
Proof state after:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
m : ℕ
k : ℕ+
hmk : ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
⊢ ∃ m k, x = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Theorem: roots_of_unity_in_cyclo
Proof state before:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
m : ℕ
k : ℕ+
hmk : ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
⊢ ∃ m k, x = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Tactic:
refine' ⟨m, k, _⟩
Proof state after:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
m : ℕ
k : ℕ+
hmk : ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
⊢ x = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Theorem: roots_of_unity_in_cyclo
Proof state before:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
m : ℕ
k : ℕ+
hmk : ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
⊢ x = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Tactic:
have eq : ((⟨x, hx⟩ : R) : K) = x := rfl
Proof state after:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
m : ℕ
k : ℕ+
hmk : ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
eq : ↑⟨x, hx⟩ = x
⊢ x = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Theorem: roots_of_unity_in_cyclo
Proof state before:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
m : ℕ
k : ℕ+
hmk : ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
eq : ↑⟨x, hx⟩ = x
⊢ x = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Tactic:
rw [← eq, hmk]
Proof state after:
no goals
Theorem: roots_of_unity_in_cyclo
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
⊢ IsIntegral ℤ x
Tactic:
refine' ⟨X ^ n - 1, _⟩
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
⊢ (X ^ n - 1).Monic ∧ eval₂ (algebraMap ℤ K) x (X ^ n - 1) = 0
Theorem: roots_of_unity_in_cyclo
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
⊢ (X ^ n - 1).Monic ∧ eval₂ (algebraMap ℤ K) x (X ^ n - 1) = 0
Tactic:
constructor
Proof state after:
case left
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
⊢ (X ^ n - 1).Monic

case right
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
⊢ eval₂ (algebraMap ℤ K) x (X ^ n - 1) = 0
Theorem: roots_of_unity_in_cyclo
Proof state before:
case left
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
⊢ (X ^ n - 1).Monic
Tactic:
exact monic_X_pow_sub_C 1 (ne_of_lt hn0).symm
Proof state after:
no goals
Theorem: roots_of_unity_in_cyclo
Proof state before:
case right
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
⊢ eval₂ (algebraMap ℤ K) x (X ^ n - 1) = 0
Tactic:
simp only [hn, eval₂_one, eval₂_X_pow, eval₂_sub, sub_self]
Proof state after:
no goals
Theorem: roots_of_unity_in_cyclo
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
⊢ ⟨x, hx⟩ ^ n = 1
Tactic:
ext
Proof state after:
case a
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
⊢ ↑(⟨x, hx⟩ ^ n) = ↑1
Theorem: roots_of_unity_in_cyclo
Proof state before:
case a
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
⊢ ↑(⟨x, hx⟩ ^ n) = ↑1
Tactic:
simp [hn]
Proof state after:
no goals
Theorem: roots_of_unity_in_cyclo
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
⊢ ∃ m k, ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Tactic:
obtain ⟨l, hl, hhl⟩ := (_root_.isRoot_of_unity_iff hn0 _).1 hxu
Proof state after:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
l : ℕ
hl : l ∈ n.divisors
hhl : (cyclotomic l ↥(integralClosure ℤ K)).IsRoot ⟨x, hx⟩
⊢ ∃ m k, ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Theorem: roots_of_unity_in_cyclo
Proof state before:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
l : ℕ
hl : l ∈ n.divisors
hhl : (cyclotomic l ↥(integralClosure ℤ K)).IsRoot ⟨x, hx⟩
⊢ ∃ m k, ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Tactic:
have hlp := roots_of_unity_in_cyclo_aux hl hx hhl hζ
Proof state after:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
l : ℕ
hl : l ∈ n.divisors
hhl : (cyclotomic l ↥(integralClosure ℤ K)).IsRoot ⟨x, hx⟩
hlp : l ∣ 2 * ↑p
⊢ ∃ m k, ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Theorem: roots_of_unity_in_cyclo
Proof state before:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
l : ℕ
hl : l ∈ n.divisors
hhl : (cyclotomic l ↥(integralClosure ℤ K)).IsRoot ⟨x, hx⟩
hlp : l ∣ 2 * ↑p
⊢ ∃ m k, ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Tactic:
have isPrimRoot : IsPrimitiveRoot (hζ.unit' : R) p := hζ.unit'_coe
Proof state after:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
l : ℕ
hl : l ∈ n.divisors
hhl : (cyclotomic l ↥(integralClosure ℤ K)).IsRoot ⟨x, hx⟩
hlp : l ∣ 2 * ↑p
isPrimRoot : IsPrimitiveRoot ↑hζ.unit' ↑p
⊢ ∃ m k, ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Theorem: roots_of_unity_in_cyclo
Proof state before:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
l : ℕ
hl : l ∈ n.divisors
hhl : (cyclotomic l ↥(integralClosure ℤ K)).IsRoot ⟨x, hx⟩
hlp : l ∣ 2 * ↑p
isPrimRoot : IsPrimitiveRoot ↑hζ.unit' ↑p
⊢ ∃ m k, ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Tactic:
have hxl : (⟨x, hx⟩ : R) ^ l = 1 :=  by
  apply isRoot_of_unity_of_root_cyclotomic _ hhl
  simp only [Nat.mem_divisors, dvd_refl, Ne, true_and_iff]
  apply pos_iff_ne_zero.1 (Nat.pos_of_mem_divisors hl)
Proof state after:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
l : ℕ
hl : l ∈ n.divisors
hhl : (cyclotomic l ↥(integralClosure ℤ K)).IsRoot ⟨x, hx⟩
hlp : l ∣ 2 * ↑p
isPrimRoot : IsPrimitiveRoot ↑hζ.unit' ↑p
hxl : ⟨x, hx⟩ ^ l = 1
⊢ ∃ m k, ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Theorem: roots_of_unity_in_cyclo
Proof state before:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
l : ℕ
hl : l ∈ n.divisors
hhl : (cyclotomic l ↥(integralClosure ℤ K)).IsRoot ⟨x, hx⟩
hlp : l ∣ 2 * ↑p
isPrimRoot : IsPrimitiveRoot ↑hζ.unit' ↑p
hxl : ⟨x, hx⟩ ^ l = 1
⊢ ∃ m k, ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Tactic:
have hxp' : (⟨x, hx⟩ : R) ^ (2 * p : ℕ) = 1 := by
  cases' hlp with hlp_w hlp_h
  rw [hlp_h, pow_mul, hxl]; simp only [one_pow]
Proof state after:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
l : ℕ
hl : l ∈ n.divisors
hhl : (cyclotomic l ↥(integralClosure ℤ K)).IsRoot ⟨x, hx⟩
hlp : l ∣ 2 * ↑p
isPrimRoot : IsPrimitiveRoot ↑hζ.unit' ↑p
hxl : ⟨x, hx⟩ ^ l = 1
hxp' : ⟨x, hx⟩ ^ (2 * ↑p) = 1
⊢ ∃ m k, ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m