internlm/Lean-Github huggingface dataset:
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
⊢ ↑(↑hζ.unit' ^ i) = (-1) ^ 2 * ζ ^ i
Tactic:
simp only [even_two, Even.neg_pow, one_pow, one_mul]
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) = ζ ^ 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
⊢ ↑(↑hζ.unit' ^ i) = ζ ^ i
Tactic:
rfl
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
hxp'' : ⟨x, hx⟩ ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑(↑hζ.unit' ^ i) = x
⊢ ↑2 = 2
Tactic:
decide
Proof state after:
no goals
Theorem: roots_of_unity_in_cyclo
Proof state before:
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
Tactic:
have hone : (-1 : R) ^ (p : ℕ) = (-1 : R) := by apply Odd.neg_one_pow hpo
Proof state after:
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
hone : (-1) ^ ↑p = -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.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
hone : (-1) ^ ↑p = -1
⊢ ∃ m k, ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Tactic:
have hxp3 : (-1 * ⟨x, hx⟩ : R) ^ (p : ℕ) = 1 := by
  rw [mul_pow, hone, hxp'']
  ring
Proof state after:
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
hone : (-1) ^ ↑p = -1
hxp3 : (-1 * ⟨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:
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
hone : (-1) ^ ↑p = -1
hxp3 : (-1 * ⟨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 hxp3 p.prop
Proof state after:
case intro.intro.inr.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
hone : (-1) ^ ↑p = -1
hxp3 : (-1 * ⟨x, hx⟩) ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑hζ.unit' ^ i = -1 * ⟨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.inr.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
hone : (-1) ^ ↑p = -1
hxp3 : (-1 * ⟨x, hx⟩) ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑hζ.unit' ^ i = -1 * ⟨x, hx⟩
⊢ ∃ m k, ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
Tactic:
refine' ⟨i, 1, _⟩
Proof state after:
case intro.intro.inr.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
hone : (-1) ^ ↑p = -1
hxp3 : (-1 * ⟨x, hx⟩) ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑hζ.unit' ^ i = -1 * ⟨x, hx⟩
⊢ ↑⟨x, hx⟩ = (-1) ^ ↑1 * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ i
Theorem: roots_of_unity_in_cyclo
Proof state before:
case intro.intro.inr.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
hone : (-1) ^ ↑p = -1
hxp3 : (-1 * ⟨x, hx⟩) ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑hζ.unit' ^ i = -1 * ⟨x, hx⟩
⊢ ↑⟨x, hx⟩ = (-1) ^ ↑1 * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ i
Tactic:
simp only [PNat.one_coe, pow_one, neg_mul, one_mul, neg_neg]
Proof state after:
case intro.intro.inr.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
hone : (-1) ^ ↑p = -1
hxp3 : (-1 * ⟨x, hx⟩) ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑hζ.unit' ^ i = -1 * ⟨x, hx⟩
⊢ x = -(algebraMap (𝓞 K) K) ↑hζ.unit' ^ i
Theorem: roots_of_unity_in_cyclo
Proof state before:
case intro.intro.inr.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
hone : (-1) ^ ↑p = -1
hxp3 : (-1 * ⟨x, hx⟩) ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑hζ.unit' ^ i = -1 * ⟨x, hx⟩
⊢ x = -(algebraMap (𝓞 K) K) ↑hζ.unit' ^ i
Tactic:
rw [← Subtype.val_inj] at Hi
Proof state after:
case intro.intro.inr.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
hone : (-1) ^ ↑p = -1
hxp3 : (-1 * ⟨x, hx⟩) ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑(↑hζ.unit' ^ i) = ↑(-1 * ⟨x, hx⟩)
⊢ x = -(algebraMap (𝓞 K) K) ↑hζ.unit' ^ i
Theorem: roots_of_unity_in_cyclo
Proof state before:
case intro.intro.inr.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
hone : (-1) ^ ↑p = -1
hxp3 : (-1 * ⟨x, hx⟩) ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑(↑hζ.unit' ^ i) = ↑(-1 * ⟨x, hx⟩)
⊢ x = -(algebraMap (𝓞 K) K) ↑hζ.unit' ^ i
Tactic:
simp only [SubmonoidClass.coe_pow, IsPrimitiveRoot.unit'_val_coe, Submonoid.coe_mul,
  Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring, InvMemClass.coe_inv,
  OneMemClass.coe_one, neg_mul, one_mul] at Hi
Proof state after:
case intro.intro.inr.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
hone : (-1) ^ ↑p = -1
hxp3 : (-1 * ⟨x, hx⟩) ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑(↑hζ.unit' ^ i) = ↑(-⟨x, hx⟩)
⊢ x = -(algebraMap (𝓞 K) K) ↑hζ.unit' ^ i
Theorem: roots_of_unity_in_cyclo
Proof state before:
case intro.intro.inr.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
hone : (-1) ^ ↑p = -1
hxp3 : (-1 * ⟨x, hx⟩) ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑(↑hζ.unit' ^ i) = ↑(-⟨x, hx⟩)
⊢ x = -(algebraMap (𝓞 K) K) ↑hζ.unit' ^ i
Tactic:
simp only [IsPrimitiveRoot.unit'_val_coe]
Proof state after:
case intro.intro.inr.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
hone : (-1) ^ ↑p = -1
hxp3 : (-1 * ⟨x, hx⟩) ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑(↑hζ.unit' ^ i) = ↑(-⟨x, hx⟩)
⊢ x = -ζ ^ i
Theorem: roots_of_unity_in_cyclo
Proof state before:
case intro.intro.inr.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
hone : (-1) ^ ↑p = -1
hxp3 : (-1 * ⟨x, hx⟩) ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑(↑hζ.unit' ^ i) = ↑(-⟨x, hx⟩)
⊢ x = -ζ ^ i
Tactic:
exact Iff.mp neg_eq_iff_eq_neg (id (Eq.symm (by simpa using Hi)))
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
hxp'' : ⟨x, hx⟩ ^ ↑p = -1
⊢ (-1) ^ ↑p = -1
Tactic:
apply Odd.neg_one_pow hpo
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
hxp'' : ⟨x, hx⟩ ^ ↑p = -1
hone : (-1) ^ ↑p = -1
⊢ (-1 * ⟨x, hx⟩) ^ ↑p = 1
Tactic:
rw [mul_pow, hone, 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⟩ ^ (2 * ↑p) = 1
hxp'' : ⟨x, hx⟩ ^ ↑p = -1
hone : (-1) ^ ↑p = -1
⊢ -1 * -1 = 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⟩ ^ (2 * ↑p) = 1
hxp'' : ⟨x, hx⟩ ^ ↑p = -1
hone : (-1) ^ ↑p = -1
⊢ -1 * -1 = 1
Tactic:
ring
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
hxp'' : ⟨x, hx⟩ ^ ↑p = -1
hone : (-1) ^ ↑p = -1
hxp3 : (-1 * ⟨x, hx⟩) ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑(↑hζ.unit' ^ i) = ↑(-⟨x, hx⟩)
⊢ ζ ^ i = -x
Tactic:
simpa using Hi
Proof state after:
no goals
Theorem: norm_cast_ne_two
Proof state before:
p : ℕ+
K : Type ?u.135468
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
⊢ ↑p ≠ 2
Tactic:
contrapose! h
Proof state after:
p : ℕ+
K : Type ?u.135468
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : ↑p = 2
⊢ p = 2
Theorem: norm_cast_ne_two
Proof state before:
p : ℕ+
K : Type ?u.135468
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : ↑p = 2
⊢ p = 2
Tactic:
exact PNat.coe_injective h
Proof state after:
no goals
Theorem: IsPrimitiveRoot.isPrime_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
⊢ (Ideal.span {↑hζ.unit' - 1}).IsPrime
Tactic:
rw [Ideal.span_singleton_prime]
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
⊢ Prime (↑hζ.unit' - 1)

p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
⊢ ↑hζ.unit' - 1 ≠ 0
Theorem: IsPrimitiveRoot.isPrime_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
⊢ ↑hζ.unit' - 1 ≠ 0
Tactic:
apply_fun (fun x : 𝓞 K => (x : K))
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
⊢ (fun x => ↑x) (↑hζ.unit' - 1) ≠ (fun x => ↑x) 0
Theorem: IsPrimitiveRoot.isPrime_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
⊢ (fun x => ↑x) (↑hζ.unit' - 1) ≠ (fun x => ↑x) 0
Tactic:
push_cast
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
⊢ ↑(↑hζ.unit' - 1) ≠ ↑0
Theorem: IsPrimitiveRoot.isPrime_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
⊢ ↑(↑hζ.unit' - 1) ≠ ↑0
Tactic:
intro h
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : ↑(↑hζ.unit' - 1) = ↑0
⊢ False
Theorem: IsPrimitiveRoot.isPrime_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : ↑(↑hζ.unit' - 1) = ↑0
⊢ False
Tactic:
simp only [map_sub, coe_unit'_coe, map_one, map_zero, sub_eq_zero] at h
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : ζ = 1
⊢ False
Theorem: IsPrimitiveRoot.isPrime_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : ζ = 1
⊢ False
Tactic:
refine hp.1.ne_one (hζ.unique ?_)
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : ζ = 1
⊢ IsPrimitiveRoot ζ 1
Theorem: IsPrimitiveRoot.isPrime_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : ζ = 1
⊢ IsPrimitiveRoot ζ 1
Tactic:
simp [h]
Proof state after:
no goals
Theorem: IsPrimitiveRoot.isPrime_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
⊢ Prime (↑hζ.unit' - 1)
Tactic:
exact hζ.zeta_sub_one_prime'
Proof state after:
no goals
Theorem: IsPrimitiveRoot.two_not_mem_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
⊢ 2 ∉ Ideal.span {↑hζ.unit' - 1}
Tactic:
have hpm := hζ.p_mem_one_sub_zeta
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
⊢ 2 ∉ Ideal.span {↑hζ.unit' - 1}
Theorem: IsPrimitiveRoot.two_not_mem_one_sub_zeta
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
⊢ 2 ∉ Ideal.span {↑hζ.unit' - 1}
Tactic:
obtain ⟨k, hk⟩ := hp.1.odd_of_ne_two (norm_cast_ne_two 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
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑p = 2 * k + 1
⊢ 2 ∉ Ideal.span {↑hζ.unit' - 1}
Theorem: IsPrimitiveRoot.two_not_mem_one_sub_zeta
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑p = 2 * k + 1
⊢ 2 ∉ Ideal.span {↑hζ.unit' - 1}
Tactic:
apply_fun (fun n : ℕ => (n : 𝓞 K)) at hk
Proof state after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑↑p = ↑(2 * k + 1)
⊢ 2 ∉ Ideal.span {↑hζ.unit' - 1}
Theorem: IsPrimitiveRoot.two_not_mem_one_sub_zeta
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑↑p = ↑(2 * k + 1)
⊢ 2 ∉ Ideal.span {↑hζ.unit' - 1}
Tactic:
rw [Nat.cast_add, Nat.cast_mul, Nat.cast_two, Nat.cast_one, add_comm] at hk
Proof state after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑↑p = 1 + 2 * ↑k
⊢ 2 ∉ Ideal.span {↑hζ.unit' - 1}