Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one (FltRegular/NumberTheory/Cyclotomic/CyclotomicUnits.lean)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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
Tactic:
rw [add_comm]
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 = ζ ^ i + -ζ ^ j

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 = ζ ^ i + -ζ ^ j
Tactic:
ring
State after:
no goals

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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
⊢ (i - j).Coprime p
Tactic:
rw [Nat.coprime_comm]
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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
⊢ p.Coprime (i - j)

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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
⊢ p.Coprime (i - j)
Tactic:
apply Nat.coprime_of_lt_prime _ _ hp
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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
⊢ 0 < i - j

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)
⊢ i - j < p

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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
⊢ 0 < i - j

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)
⊢ i - j < p
Tactic:
apply Nat.sub_pos_of_lt hilj
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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
⊢ i - j < p

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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
⊢ i - j < p
Tactic:
by_cases hj : 0 < j
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)
hj : 0 < j
⊢ i - j < p

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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hj : ¬0 < j
⊢ i - j < p

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)
hj : 0 < j
⊢ i - j < p

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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hj : ¬0 < j
⊢ i - j < p
Tactic:
apply lt_trans _ hi
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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hj : 0 < j
⊢ i - j < i

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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hj : ¬0 < j
⊢ i - j < p

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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hj : 0 < j
⊢ i - j < i

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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hj : ¬0 < j
⊢ i - j < p
Tactic:
apply Nat.sub_lt_of_pos_le hj hilj.le
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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hj : ¬0 < j
⊢ i - j < p

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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hj : ¬0 < j
⊢ i - j < p
Tactic:
simp only [not_lt, _root_.le_zero_iff] at hj
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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hj : j = 0
⊢ i - j < p

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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hj : j = 0
⊢ i - j < p
Tactic:
rw [hj]
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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hj : j = 0
⊢ i - 0 < p

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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hj : j = 0
⊢ i - 0 < p
Tactic:
simp only [tsub_zero]
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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hj : j = 0
⊢ i < p

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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hj : j = 0
⊢ i < p
Tactic:
exact hi
State after:
no goals

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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hic : (i - j).Coprime p
⊢ IsUnit (-ζ ^ j * ∑ k ∈ range (i - j), ζ ^ k)
Tactic:
apply IsUnit.mul _ (IsPrimitiveRoot.sum_pow_unit _ hn hic hζ)
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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hic : (i - j).Coprime p
⊢ IsUnit (-ζ ^ j)

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
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hic : (i - j).Coprime p
⊢ IsUnit (-ζ ^ j)
Tactic:
apply IsUnit.neg
State after:
case a
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
⊢ IsUnit (ζ ^ j)

State before:
case a
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
⊢ IsUnit (ζ ^ j)
Tactic:
apply IsUnit.pow
State after:
case a.a
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
⊢ IsUnit ζ

State before:
case a.a
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
⊢ IsUnit ζ
Tactic:
apply hζ.isUnit hp.pos
State after:
no goals

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 : i ≤ j
⊢ ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
Tactic:
ring_nf
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 : i ≤ j
⊢ ζ ^ i - ζ ^ j = ζ ^ i - ζ ^ i * ζ ^ (j - i)

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 : i ≤ j
⊢ ζ ^ i - ζ ^ j = ζ ^ i - ζ ^ i * ζ ^ (j - i)
Tactic:
simp
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 : i ≤ j
⊢ ζ ^ j = ζ ^ i * ζ ^ (j - i)

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 : i ≤ j
⊢ ζ ^ j = ζ ^ i * ζ ^ (j - i)
Tactic:
rw [pow_mul_pow_sub _ hilj]
State after:
no goals

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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
⊢ (j - i).Coprime p
Tactic:
rw [Nat.coprime_comm]
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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
⊢ p.Coprime (j - i)

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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
⊢ p.Coprime (j - i)
Tactic:
apply Nat.coprime_of_lt_prime _ _ hp
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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
⊢ 0 < j - i

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)
⊢ j - i < p

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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
⊢ 0 < j - i

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)
⊢ j - i < p
Tactic:
have hilj' : i < j := by rw [lt_iff_le_and_ne]; simp [hij, hilj]
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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hilj' : i < j
⊢ 0 < j - i

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)
⊢ j - i < p

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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hilj' : i < j
⊢ 0 < j - i

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)
⊢ j - i < p
Tactic:
apply Nat.sub_pos_of_lt hilj'
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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
⊢ j - i < p

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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
⊢ j - i < p
Tactic:
by_cases hii : 0 < i
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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hii : 0 < i
⊢ j - i < p

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)
hii : ¬0 < i
⊢ j - i < p

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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hii : 0 < i
⊢ j - i < p

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)
hii : ¬0 < i
⊢ j - i < p
Tactic:
apply lt_trans _ hj
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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hii : 0 < i
⊢ j - 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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hii : ¬0 < i
⊢ j - i < p

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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hii : 0 < i
⊢ j - 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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hii : ¬0 < i
⊢ j - i < p
Tactic:
apply Nat.sub_lt_of_pos_le hii hilj
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)
hii : ¬0 < i
⊢ j - i < p

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)
hii : ¬0 < i
⊢ j - i < p
Tactic:
simp only [not_lt, _root_.le_zero_iff] at hii
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)
hii : i = 0
⊢ j - i < p

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)
hii : i = 0
⊢ j - i < p
Tactic:
rw [hii]
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)
hii : i = 0
⊢ j - 0 < p

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)
hii : i = 0
⊢ j - 0 < p
Tactic:
simp only [tsub_zero]
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)
hii : i = 0
⊢ j < p

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)
hii : i = 0
⊢ j < p
Tactic:
exact hj
State after:
no goals

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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
⊢ i < j
Tactic:
rw [lt_iff_le_and_ne]
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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
⊢ i ≤ j ∧ i ≠ j

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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
⊢ i ≤ j ∧ i ≠ j
Tactic:
simp [hij, hilj]
State after:
no goals

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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hjc : (j - i).Coprime p
⊢ IsUnit (ζ ^ i * ∑ k ∈ range (j - i), ζ ^ k)
Tactic:
apply IsUnit.mul _ (IsPrimitiveRoot.sum_pow_unit _ hn hjc hζ)
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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hjc : (j - i).Coprime p
⊢ IsUnit (ζ ^ i)

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 : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hjc : (j - i).Coprime p
⊢ IsUnit (ζ ^ i)
Tactic:
apply IsUnit.pow
State after:
case a
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
⊢ IsUnit ζ

State before:
case a
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
⊢ IsUnit ζ
Tactic:
apply hζ.isUnit hp.pos
State after:
no goals