internlm/Lean-Github huggingface dataset:
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
⊢ ζ ^ i - ζ ^ j = -ζ ^ j + ζ ^ i
Tactic:
rw [add_comm]
Proof state after:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
⊢ ζ ^ i - ζ ^ j = ζ ^ i + -ζ ^ j
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
⊢ ζ ^ i - ζ ^ j = ζ ^ i + -ζ ^ j
Tactic:
ring
Proof state after:
no goals
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
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]
Proof state after:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
⊢ p.Coprime (i - j)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
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
Proof state after:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
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
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
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
Proof state after:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
⊢ i - j < p
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
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
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)
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
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)
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
Proof state after:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj✝ : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
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
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj✝ : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
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
Proof state after:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj✝ : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hj : ¬0 < j
⊢ i - j < p
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj✝ : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
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
Proof state after:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj✝ : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hj : j = 0
⊢ i - j < p
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj✝ : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
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]
Proof state after:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj✝ : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hj : j = 0
⊢ i - 0 < p
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj✝ : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
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]
Proof state after:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj✝ : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hj : j = 0
⊢ i < p
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj✝ : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
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
Proof state after:
no goals
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
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ζ)
Proof state after:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
h1 : ζ ^ i - ζ ^ j = ζ ^ j * (ζ ^ (i - j) - 1)
h2 : (1 - ζ) * ∑ i ∈ range (i - j), ζ ^ i = 1 - ζ ^ (i - j)
hic : (i - j).Coprime p
⊢ IsUnit (-ζ ^ j)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : i ≠ j
hζ : IsPrimitiveRoot ζ p
hilj : j < i
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
Proof 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)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof 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
Proof 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 ζ
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof 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
Proof state after:
no goals
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
⊢ ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
Tactic:
ring_nf
Proof state after:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
⊢ ζ ^ i - ζ ^ j = ζ ^ i - ζ ^ i * ζ ^ (j - i)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
⊢ ζ ^ i - ζ ^ j = ζ ^ i - ζ ^ i * ζ ^ (j - i)
Tactic:
simp
Proof state after:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
⊢ ζ ^ j = ζ ^ i * ζ ^ (j - i)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one
Proof state before:
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
⊢ ζ ^ j = ζ ^ i * ζ ^ (j - i)
Tactic:
rw [pow_mul_pow_sub _ hilj]
Proof state after:
no goals