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 : 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]
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
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
⊢ p.Coprime (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
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
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
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
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
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]
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
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
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
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'
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
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
⊢ j - i < 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 : 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
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 : 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
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 : 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
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
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
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
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
Proof state after:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hii : ¬0 < i
⊢ j - 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 : 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
Proof state after:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hii : i = 0
⊢ j - 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 : 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]
Proof state after:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hii : i = 0
⊢ j - 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 : 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]
Proof state after:
case neg
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p i j : ℕ
ζ : A
hn : 2 ≤ p
hp : p.Prime
hi : i < p
hj : j < p
hij : ¬i = j
hζ : IsPrimitiveRoot ζ p
hilj : i ≤ j
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hii : i = 0
⊢ 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 : 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
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
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]
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
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (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 : 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]
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
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ζ)
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
h1 : ζ ^ i - ζ ^ j = ζ ^ i * (1 - ζ ^ (j - i))
h2 : (1 - ζ) * ∑ i ∈ range (j - i), ζ ^ i = 1 - ζ ^ (j - i)
hjc : (j - i).Coprime p
⊢ IsUnit (ζ ^ 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
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
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 : 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 ζ
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 : 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
Proof state after:
no goals
Theorem: IsPrimitiveRoot.associated_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
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
η₁ : A
hη₁ : η₁ ∈ nthRootsFinset p A
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p A
e : η₁ ≠ η₂
⊢ Associated (ζ - 1) (η₁ - η₂)
Tactic:
obtain ⟨i, ⟨hi, rfl⟩⟩ := hζ.eq_pow_of_pow_eq_one ((Polynomial.mem_nthRootsFinset hp.pos).1 hη₁) hp.pos
Proof state after:
case intro.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
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p A
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ nthRootsFinset p A
e : ζ ^ i ≠ η₂
⊢ Associated (ζ - 1) (ζ ^ i - η₂)
Theorem: IsPrimitiveRoot.associated_sub_one
Proof state before:
case intro.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
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p A
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ nthRootsFinset p A
e : ζ ^ i ≠ η₂
⊢ Associated (ζ - 1) (ζ ^ i - η₂)
Tactic:
obtain ⟨j, ⟨hj, rfl⟩⟩ := hζ.eq_pow_of_pow_eq_one ((Polynomial.mem_nthRootsFinset hp.pos).1 hη₂) hp.pos
Proof state after:
case intro.intro.intro.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
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ nthRootsFinset p A
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ nthRootsFinset p A
e : ζ ^ i ≠ ζ ^ j
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)