internlm/Lean-Github huggingface dataset:
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
case h
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (∑ i ∈ range (i - j), ζ ^ i) * (1 - ζ) = 1 - ζ ^ (i - j)
hic : (i - j).Coprime p
v : Aˣ
hv : ↑v = -ζ ^ j * ∑ k ∈ range (i - j), ζ ^ k
⊢ ζ ^ j * (ζ ^ (i - j) - 1) = (-ζ ^ j * ∑ k ∈ range (i - j), ζ ^ k) * (1 - ζ)

case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : ¬j < i
⊢ ∃ u, ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
Tactic:
rw [mul_assoc]
Proof state after:
case h
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (∑ i ∈ range (i - j), ζ ^ i) * (1 - ζ) = 1 - ζ ^ (i - j)
hic : (i - j).Coprime p
v : Aˣ
hv : ↑v = -ζ ^ j * ∑ k ∈ range (i - j), ζ ^ k
⊢ ζ ^ j * (ζ ^ (i - j) - 1) = -ζ ^ j * ((∑ k ∈ range (i - j), ζ ^ k) * (1 - ζ))

case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : ¬j < i
⊢ ∃ u, ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
case h
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (∑ i ∈ range (i - j), ζ ^ i) * (1 - ζ) = 1 - ζ ^ (i - j)
hic : (i - j).Coprime p
v : Aˣ
hv : ↑v = -ζ ^ j * ∑ k ∈ range (i - j), ζ ^ k
⊢ ζ ^ j * (ζ ^ (i - j) - 1) = -ζ ^ j * ((∑ k ∈ range (i - j), ζ ^ k) * (1 - ζ))

case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : ¬j < i
⊢ ∃ u, ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
Tactic:
rw [h2]
Proof state after:
case h
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (∑ i ∈ range (i - j), ζ ^ i) * (1 - ζ) = 1 - ζ ^ (i - j)
hic : (i - j).Coprime p
v : Aˣ
hv : ↑v = -ζ ^ j * ∑ k ∈ range (i - j), ζ ^ k
⊢ ζ ^ j * (ζ ^ (i - j) - 1) = -ζ ^ j * (1 - ζ ^ (i - j))

case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : ¬j < i
⊢ ∃ u, ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
case h
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (∑ i ∈ range (i - j), ζ ^ i) * (1 - ζ) = 1 - ζ ^ (i - j)
hic : (i - j).Coprime p
v : Aˣ
hv : ↑v = -ζ ^ j * ∑ k ∈ range (i - j), ζ ^ k
⊢ ζ ^ j * (ζ ^ (i - j) - 1) = -ζ ^ j * (1 - ζ ^ (i - j))

case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : ¬j < i
⊢ ∃ u, ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
Tactic:
ring
Proof state after:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : ¬j < i
⊢ ∃ u, ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : ¬j < i
⊢ ∃ u, ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
Tactic:
simp at *
Proof state after:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
⊢ ∃ u, ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
⊢ ∃ u, ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
Tactic:
have h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i)) := by
  ring_nf
  simp; rw [pow_mul_pow_sub _ hilj]
Proof state after:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
⊢ ∃ u, ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
⊢ ∃ u, ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
Tactic:
rw [h1]
Proof state after:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
⊢ ∃ u, ζ ^ i * (1 - ζ ^ (j - i)) = ↑u * (1 - ζ)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
⊢ ∃ u, ζ ^ i * (1 - ζ ^ (j - i)) = ↑u * (1 - ζ)
Tactic:
have h2 := mul_neg_geom_sum ζ (j - i)
Proof state after:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
⊢ ∃ u, ζ ^ i * (1 - ζ ^ (j - i)) = ↑u * (1 - ζ)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
⊢ ∃ u, ζ ^ i * (1 - ζ ^ (j - i)) = ↑u * (1 - ζ)
Tactic:
have hjc : (j - i).Coprime p := by
  rw [Nat.coprime_comm]
  apply Nat.coprime_of_lt_prime _ _ hp
  have hilj' : i < j := by rw [lt_iff_le_and_ne]; simp [hij, hilj]
  apply Nat.sub_pos_of_lt hilj'
  by_cases hii : 0 < i
  apply lt_trans _ hj
  apply Nat.sub_lt_of_pos_le hii hilj
  simp only [not_lt, _root_.le_zero_iff] at hii
  rw [hii]
  simp only [tsub_zero]
  exact hj
Proof state after:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hjc : (j - i).Coprime p
⊢ ∃ u, ζ ^ i * (1 - ζ ^ (j - i)) = ↑u * (1 - ζ)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hjc : (j - i).Coprime p
⊢ ∃ u, ζ ^ i * (1 - ζ ^ (j - i)) = ↑u * (1 - ζ)
Tactic:
have h3 : IsUnit (ζ ^ i * ∑ k : ℕ in range (j - i), ζ ^ (k : ℕ)) := by
  apply IsUnit.mul _ (IsPrimitiveRoot.sum_pow_unit _ hn hjc hζ); apply IsUnit.pow
  apply hζ.isUnit hp.pos
Proof state after:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hjc : (j - i).Coprime p
h3 : IsUnit (ζ ^ i * ∑ k ∈ range (j - i), ζ ^ k)
⊢ ∃ u, ζ ^ i * (1 - ζ ^ (j - i)) = ↑u * (1 - ζ)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hjc : (j - i).Coprime p
h3 : IsUnit (ζ ^ i * ∑ k ∈ range (j - i), ζ ^ k)
⊢ ∃ u, ζ ^ i * (1 - ζ ^ (j - i)) = ↑u * (1 - ζ)
Tactic:
obtain ⟨v, hv⟩ := h3
Proof state after:
case neg.intro
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hjc : (j - i).Coprime p
v : Aˣ
hv : ↑v = ζ ^ i * ∑ k ∈ range (j - i), ζ ^ k
⊢ ∃ u, ζ ^ i * (1 - ζ ^ (j - i)) = ↑u * (1 - ζ)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
case neg.intro
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hjc : (j - i).Coprime p
v : Aˣ
hv : ↑v = ζ ^ i * ∑ k ∈ range (j - i), ζ ^ k
⊢ ∃ u, ζ ^ i * (1 - ζ ^ (j - i)) = ↑u * (1 - ζ)
Tactic:
use v
Proof state after:
case h
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hjc : (j - i).Coprime p
v : Aˣ
hv : ↑v = ζ ^ i * ∑ k ∈ range (j - i), ζ ^ k
⊢ ζ ^ i * (1 - ζ ^ (j - i)) = ↑v * (1 - ζ)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
case h
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hjc : (j - i).Coprime p
v : Aˣ
hv : ↑v = ζ ^ i * ∑ k ∈ range (j - i), ζ ^ k
⊢ ζ ^ i * (1 - ζ ^ (j - i)) = ↑v * (1 - ζ)
Tactic:
rw [hv]
Proof state after:
case h
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hjc : (j - i).Coprime p
v : Aˣ
hv : ↑v = ζ ^ i * ∑ k ∈ range (j - i), ζ ^ k
⊢ ζ ^ i * (1 - ζ ^ (j - i)) = (ζ ^ i * ∑ k ∈ range (j - i), ζ ^ k) * (1 - ζ)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
case h
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hjc : (j - i).Coprime p
v : Aˣ
hv : ↑v = ζ ^ i * ∑ k ∈ range (j - i), ζ ^ k
⊢ ζ ^ i * (1 - ζ ^ (j - i)) = (ζ ^ i * ∑ k ∈ range (j - i), ζ ^ k) * (1 - ζ)
Tactic:
rw [mul_comm] at h2
Proof state after:
case h
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (∑ i ∈ range (j - i), ζ ^ i) * (1 - ζ) = 1 - ζ ^ (j - i)
hjc : (j - i).Coprime p
v : Aˣ
hv : ↑v = ζ ^ i * ∑ k ∈ range (j - i), ζ ^ k
⊢ ζ ^ i * (1 - ζ ^ (j - i)) = (ζ ^ i * ∑ k ∈ range (j - i), ζ ^ k) * (1 - ζ)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
case h
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (∑ i ∈ range (j - i), ζ ^ i) * (1 - ζ) = 1 - ζ ^ (j - i)
hjc : (j - i).Coprime p
v : Aˣ
hv : ↑v = ζ ^ i * ∑ k ∈ range (j - i), ζ ^ k
⊢ ζ ^ i * (1 - ζ ^ (j - i)) = (ζ ^ i * ∑ k ∈ range (j - i), ζ ^ k) * (1 - ζ)
Tactic:
rw [mul_assoc]
Proof state after:
case h
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (∑ i ∈ range (j - i), ζ ^ i) * (1 - ζ) = 1 - ζ ^ (j - i)
hjc : (j - i).Coprime p
v : Aˣ
hv : ↑v = ζ ^ i * ∑ k ∈ range (j - i), ζ ^ k
⊢ ζ ^ i * (1 - ζ ^ (j - i)) = ζ ^ i * ((∑ k ∈ range (j - i), ζ ^ k) * (1 - ζ))
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
case h
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (∑ i ∈ range (j - i), ζ ^ i) * (1 - ζ) = 1 - ζ ^ (j - i)
hjc : (j - i).Coprime p
v : Aˣ
hv : ↑v = ζ ^ i * ∑ k ∈ range (j - i), ζ ^ k
⊢ ζ ^ i * (1 - ζ ^ (j - i)) = ζ ^ i * ((∑ k ∈ range (j - i), ζ ^ k) * (1 - ζ))
Tactic:
rw [h2]
Proof state after:
no goals
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
⊢ ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
Tactic:
ring_nf
Proof state after:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
⊢ ζ ^ i - ζ ^ j = -ζ ^ j + ζ ^ j * ζ ^ (i - j)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
⊢ ζ ^ i - ζ ^ j = -ζ ^ j + ζ ^ j * ζ ^ (i - j)
Tactic:
rw [pow_mul_pow_sub _ hilj.le]
Proof state after:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
⊢ ζ ^ i - ζ ^ j = -ζ ^ j + ζ ^ i