internlm/Lean-Github huggingface dataset:
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit
Proof state before:
case h.e'_3.inr
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
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
h2 : 1 = ζ
hn1 : 1 < n
h1 this : True
hp : ¬1 = 1
⊢ False
Tactic:
simp only [eq_self_iff_true, not_true] at hp
Proof state after:
no goals
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit
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
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
h2 : 1 - ζ = 0
⊢ 1 < n
Tactic:
linarith
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
⊢ ∃ u, ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
Tactic:
by_cases hilj : j < i
Proof state after:
case pos
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 - ζ)

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

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:
have h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1) := by
  ring_nf
  rw [pow_mul_pow_sub _ hilj.le]
  rw [add_comm]
  ring
Proof state after:
case pos
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)
⊢ ∃ u, ζ ^ i - ζ ^ j = ↑u * (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 pos
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)
⊢ ∃ u, ζ ^ i - ζ ^ j = ↑u * (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 [h1]
Proof state after:
case pos
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)
⊢ ∃ u, ζ ^ j * (ζ ^ (i - j) - 1) = ↑u * (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 pos
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)
⊢ ∃ u, ζ ^ j * (ζ ^ (i - j) - 1) = ↑u * (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:
have h2 := mul_neg_geom_sum ζ (i - j)
Proof state after:
case pos
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 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
⊢ ∃ u, ζ ^ j * (ζ ^ (i - j) - 1) = ↑u * (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 pos
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 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
⊢ ∃ u, ζ ^ j * (ζ ^ (i - j) - 1) = ↑u * (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:
have hic : (i - j).Coprime p := by
  rw [Nat.coprime_comm]; apply Nat.coprime_of_lt_prime _ _ hp
  apply Nat.sub_pos_of_lt hilj
  by_cases hj : 0 < j
  apply lt_trans _ hi
  apply Nat.sub_lt_of_pos_le hj hilj.le
  simp only [not_lt, _root_.le_zero_iff] at hj
  rw [hj]
  simp only [tsub_zero]
  exact hi
Proof state after:
case pos
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 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hic : (i - j).Coprime p
⊢ ∃ u, ζ ^ j * (ζ ^ (i - j) - 1) = ↑u * (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 pos
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 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hic : (i - j).Coprime p
⊢ ∃ u, ζ ^ j * (ζ ^ (i - j) - 1) = ↑u * (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:
have h3 : IsUnit (-ζ ^ j * ∑ k : ℕ in range (i - j), ζ ^ (k : ℕ)) := by
  apply IsUnit.mul _ (IsPrimitiveRoot.sum_pow_unit _ hn hic hζ); apply IsUnit.neg
  apply IsUnit.pow; apply hζ.isUnit hp.pos
Proof state after:
case pos
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 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hic : (i - j).Coprime p
h3 : IsUnit (-ζ ^ j * ∑ k ∈ range (i - j), ζ ^ k)
⊢ ∃ u, ζ ^ j * (ζ ^ (i - j) - 1) = ↑u * (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 pos
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 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hic : (i - j).Coprime p
h3 : IsUnit (-ζ ^ j * ∑ k ∈ range (i - j), ζ ^ k)
⊢ ∃ u, ζ ^ j * (ζ ^ (i - j) - 1) = ↑u * (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:
obtain ⟨v, hv⟩ := h3
Proof state after:
case pos.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 : j < i
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hic : (i - j).Coprime p
v : Aˣ
hv : ↑v = -ζ ^ j * ∑ k ∈ range (i - j), ζ ^ k
⊢ ∃ u, ζ ^ j * (ζ ^ (i - j) - 1) = ↑u * (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 pos.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 : j < i
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hic : (i - j).Coprime p
v : Aˣ
hv : ↑v = -ζ ^ j * ∑ k ∈ range (i - j), ζ ^ k
⊢ ∃ u, ζ ^ j * (ζ ^ (i - j) - 1) = ↑u * (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:
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 : j < i
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hic : (i - j).Coprime p
v : Aˣ
hv : ↑v = -ζ ^ j * ∑ k ∈ range (i - j), ζ ^ k
⊢ ζ ^ j * (ζ ^ (i - j) - 1) = ↑v * (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 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hic : (i - j).Coprime p
v : Aˣ
hv : ↑v = -ζ ^ j * ∑ k ∈ range (i - j), ζ ^ k
⊢ ζ ^ j * (ζ ^ (i - j) - 1) = ↑v * (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 [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 : j < i
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 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 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 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_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 : 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 - ζ)