Theorem: roots_of_unity_in_cyclo (FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean)

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
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

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]
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

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
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

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, _⟩
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

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
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

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]
State after:
no goals

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, _⟩
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

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
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

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
State after:
no goals

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]
State after:
no goals

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
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

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]
State after:
no goals

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
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

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ζ
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

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
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

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)
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

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]
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

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''
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

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
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

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]
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

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)
State after:
no goals

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
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

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]
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

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]
State after:
no goals

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'
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

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'
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

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
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

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]
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

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'
State after:
no goals

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
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

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
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

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]
State after:
no goals

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
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

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]
State after:
no goals

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
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

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, _⟩
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

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]
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

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
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

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
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

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]
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

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]
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

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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
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

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, _⟩
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

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]
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

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
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

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
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

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]
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

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)))
State after:
no goals

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
State after:
no goals

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'']
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

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
State after:
no goals

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
State after:
no goals