internlm/Lean-Github huggingface dataset:
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
hxp' : ⟨x, hx⟩ ^ (2 * ↑p) = 1
hxp'' : ⟨x, hx⟩ ^ ↑p = 1 ∨ ⟨x, hx⟩ ^ ↑p = -1
⊢ ∃ m k, ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Tactic:
cases' hxp'' with hxp'' hxp''
Proof state after:
case intro.intro.inl
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
hxp'' : ⟨x, hx⟩ ^ ↑p = 1
⊢ ∃ m k, ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m

case intro.intro.inr
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
hxp'' : ⟨x, hx⟩ ^ ↑p = -1
⊢ ∃ m k, ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
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
l : ℕ
hl : l ∈ n.divisors
hhl : (cyclotomic l ↥(integralClosure ℤ K)).IsRoot ⟨x, hx⟩
hlp : l ∣ 2 * ↑p
isPrimRoot : IsPrimitiveRoot ↑hζ.unit' ↑p
⊢ ⟨x, hx⟩ ^ l = 1
Tactic:
apply isRoot_of_unity_of_root_cyclotomic _ hhl
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
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
⊢ l ∈ l.divisors
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
l : ℕ
hl : l ∈ n.divisors
hhl : (cyclotomic l ↥(integralClosure ℤ K)).IsRoot ⟨x, hx⟩
hlp : l ∣ 2 * ↑p
isPrimRoot : IsPrimitiveRoot ↑hζ.unit' ↑p
⊢ l ∈ l.divisors
Tactic:
simp only [Nat.mem_divisors, dvd_refl, Ne, true_and_iff]
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
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
⊢ ¬l = 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
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
⊢ ¬l = 0
Tactic:
apply pos_iff_ne_zero.1 (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
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
⊢ ⟨x, hx⟩ ^ (2 * ↑p) = 1
Tactic:
cases' hlp with hlp_w hlp_h
Proof state after:
case 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⟩
isPrimRoot : IsPrimitiveRoot ↑hζ.unit' ↑p
hxl : ⟨x, hx⟩ ^ l = 1
hlp_w : ℕ
hlp_h : 2 * ↑p = l * hlp_w
⊢ ⟨x, hx⟩ ^ (2 * ↑p) = 1
Theorem: roots_of_unity_in_cyclo
Proof state before:
case 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⟩
isPrimRoot : IsPrimitiveRoot ↑hζ.unit' ↑p
hxl : ⟨x, hx⟩ ^ l = 1
hlp_w : ℕ
hlp_h : 2 * ↑p = l * hlp_w
⊢ ⟨x, hx⟩ ^ (2 * ↑p) = 1
Tactic:
rw [hlp_h, pow_mul, hxl]
Proof state after:
case 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⟩
isPrimRoot : IsPrimitiveRoot ↑hζ.unit' ↑p
hxl : ⟨x, hx⟩ ^ l = 1
hlp_w : ℕ
hlp_h : 2 * ↑p = l * hlp_w
⊢ 1 ^ hlp_w = 1
Theorem: roots_of_unity_in_cyclo
Proof state before:
case 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⟩
isPrimRoot : IsPrimitiveRoot ↑hζ.unit' ↑p
hxl : ⟨x, hx⟩ ^ l = 1
hlp_w : ℕ
hlp_h : 2 * ↑p = l * hlp_w
⊢ 1 ^ hlp_w = 1
Tactic:
simp only [one_pow]
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
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
⊢ ⟨x, hx⟩ ^ ↑p = 1 ∨ ⟨x, hx⟩ ^ ↑p = -1
Tactic:
rw [mul_comm] at hxp'
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
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⟩ ^ (↑p * 2) = 1
⊢ ⟨x, hx⟩ ^ ↑p = 1 ∨ ⟨x, hx⟩ ^ ↑p = -1
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
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⟩ ^ (↑p * 2) = 1
⊢ ⟨x, hx⟩ ^ ↑p = 1 ∨ ⟨x, hx⟩ ^ ↑p = -1
Tactic:
rw [pow_mul] at hxp'
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
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⟩ ^ ↑p) ^ 2 = 1
⊢ ⟨x, hx⟩ ^ ↑p = 1 ∨ ⟨x, hx⟩ ^ ↑p = -1
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
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⟩ ^ ↑p) ^ 2 = 1
⊢ ⟨x, hx⟩ ^ ↑p = 1 ∨ ⟨x, hx⟩ ^ ↑p = -1
Tactic:
apply eq_or_eq_neg_of_sq_eq_sq
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
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⟩ ^ ↑p) ^ 2 = 1
⊢ (⟨x, hx⟩ ^ ↑p) ^ 2 = 1 ^ 2
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
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⟩ ^ ↑p) ^ 2 = 1
⊢ (⟨x, hx⟩ ^ ↑p) ^ 2 = 1 ^ 2
Tactic:
simp only [one_pow]
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
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⟩ ^ ↑p) ^ 2 = 1
⊢ (⟨x, hx⟩ ^ ↑p) ^ 2 = 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
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⟩ ^ ↑p) ^ 2 = 1
⊢ (⟨x, hx⟩ ^ ↑p) ^ 2 = 1
Tactic:
apply hxp'
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
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⟩ ^ ↑p) ^ 2 = 1
this : ⟨x, hx⟩ ^ ↑p = 1 ∨ ⟨x, hx⟩ ^ ↑p = -1
⊢ ⟨x, hx⟩ ^ ↑p = 1 ∨ ⟨x, hx⟩ ^ ↑p = -1
Tactic:
cases' this with h1 h2
Proof state after:
case inl
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⟩ ^ ↑p) ^ 2 = 1
h1 : ⟨x, hx⟩ ^ ↑p = 1
⊢ ⟨x, hx⟩ ^ ↑p = 1 ∨ ⟨x, hx⟩ ^ ↑p = -1

case inr
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⟩ ^ ↑p) ^ 2 = 1
h2 : ⟨x, hx⟩ ^ ↑p = -1
⊢ ⟨x, hx⟩ ^ ↑p = 1 ∨ ⟨x, hx⟩ ^ ↑p = -1
Theorem: roots_of_unity_in_cyclo
Proof state before:
case inl
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⟩ ^ ↑p) ^ 2 = 1
h1 : ⟨x, hx⟩ ^ ↑p = 1
⊢ ⟨x, hx⟩ ^ ↑p = 1 ∨ ⟨x, hx⟩ ^ ↑p = -1
Tactic:
left
Proof state after:
case inl.h
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⟩ ^ ↑p) ^ 2 = 1
h1 : ⟨x, hx⟩ ^ ↑p = 1
⊢ ⟨x, hx⟩ ^ ↑p = 1
Theorem: roots_of_unity_in_cyclo
Proof state before:
case inl.h
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⟩ ^ ↑p) ^ 2 = 1
h1 : ⟨x, hx⟩ ^ ↑p = 1
⊢ ⟨x, hx⟩ ^ ↑p = 1
Tactic:
simp only [h1]
Proof state after:
no goals
Theorem: roots_of_unity_in_cyclo
Proof state before:
case inr
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⟩ ^ ↑p) ^ 2 = 1
h2 : ⟨x, hx⟩ ^ ↑p = -1
⊢ ⟨x, hx⟩ ^ ↑p = 1 ∨ ⟨x, hx⟩ ^ ↑p = -1
Tactic:
right
Proof state after:
case inr.h
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⟩ ^ ↑p) ^ 2 = 1
h2 : ⟨x, hx⟩ ^ ↑p = -1
⊢ ⟨x, hx⟩ ^ ↑p = -1
Theorem: roots_of_unity_in_cyclo
Proof state before:
case inr.h
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⟩ ^ ↑p) ^ 2 = 1
h2 : ⟨x, hx⟩ ^ ↑p = -1
⊢ ⟨x, hx⟩ ^ ↑p = -1
Tactic:
simp only [h2]
Proof state after:
no goals
Theorem: roots_of_unity_in_cyclo
Proof state before:
case intro.intro.inl
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
hxp'' : ⟨x, hx⟩ ^ ↑p = 1
⊢ ∃ m k, ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Tactic:
obtain ⟨i, _, Hi⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one isPrimRoot hxp'' p.prop
Proof state after:
case intro.intro.inl.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
hxp'' : ⟨x, hx⟩ ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑hζ.unit' ^ i = ⟨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.inl.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
hxp'' : ⟨x, hx⟩ ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑hζ.unit' ^ i = ⟨x, hx⟩
⊢ ∃ m k, ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Tactic:
refine' ⟨i, 2, _⟩
Proof state after:
case intro.intro.inl.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
hxp'' : ⟨x, hx⟩ ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑hζ.unit' ^ i = ⟨x, hx⟩
⊢ ↑⟨x, hx⟩ = (-1) ^ ↑2 * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ i
Theorem: roots_of_unity_in_cyclo
Proof state before:
case intro.intro.inl.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
hxp'' : ⟨x, hx⟩ ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑hζ.unit' ^ i = ⟨x, hx⟩
⊢ ↑⟨x, hx⟩ = (-1) ^ ↑2 * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ i
Tactic:
simp only [IsPrimitiveRoot.unit'_val_coe]
Proof state after:
case intro.intro.inl.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
hxp'' : ⟨x, hx⟩ ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑hζ.unit' ^ i = ⟨x, hx⟩
⊢ x = (-1) ^ ↑2 * ζ ^ i
Theorem: roots_of_unity_in_cyclo
Proof state before:
case intro.intro.inl.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
hxp'' : ⟨x, hx⟩ ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑hζ.unit' ^ i = ⟨x, hx⟩
⊢ x = (-1) ^ ↑2 * ζ ^ i
Tactic:
rw [← Subtype.val_inj] at Hi
Proof state after:
case intro.intro.inl.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
hxp'' : ⟨x, hx⟩ ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑(↑hζ.unit' ^ i) = ↑⟨x, hx⟩
⊢ x = (-1) ^ ↑2 * ζ ^ i
Theorem: roots_of_unity_in_cyclo
Proof state before:
case intro.intro.inl.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
hxp'' : ⟨x, hx⟩ ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑(↑hζ.unit' ^ i) = ↑⟨x, hx⟩
⊢ x = (-1) ^ ↑2 * ζ ^ i
Tactic:
simp only [SubmonoidClass.coe_pow, IsPrimitiveRoot.unit'_val_coe] at Hi
Proof state after:
case intro.intro.inl.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
hxp'' : ⟨x, hx⟩ ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑(↑hζ.unit' ^ i) = x
⊢ x = (-1) ^ ↑2 * ζ ^ i
Theorem: roots_of_unity_in_cyclo
Proof state before:
case intro.intro.inl.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
hxp'' : ⟨x, hx⟩ ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑(↑hζ.unit' ^ i) = x
⊢ x = (-1) ^ ↑2 * ζ ^ i
Tactic:
rw [← Hi, show ((2 : ℕ+) : ℕ) = 2 by decide]
Proof state after:
case intro.intro.inl.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
hxp'' : ⟨x, hx⟩ ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑(↑hζ.unit' ^ i) = x
⊢ ↑(↑hζ.unit' ^ i) = (-1) ^ 2 * ζ ^ i