internlm/Lean-Github huggingface dataset:
Theorem: IsCyclotomicExtension.CyclotomicUnit.associated_one_sub_pow_primitive_root_of_coprime
Proof state before:
case h
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : 1 < n
m : ℕ
hm : j * m % n = 1
this : ζ = (ζ ^ j) ^ m
⊢ 1 - (ζ ^ j) ^ m = (1 - ζ ^ j) * ∑ i ∈ range m, (ζ ^ j) ^ i
Tactic:
rw [← geom_sum_mul_neg, mul_comm]
Proof state after:
no goals
Theorem: IsCyclotomicExtension.CyclotomicUnit.associated_one_sub_pow_primitive_root_of_coprime
Proof state before:
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n j k : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
hk : k.Coprime n
hj : j.Coprime n
this : ∀ {j : ℕ}, j.Coprime n → Associated (1 - ζ) (1 - ζ ^ j)
⊢ Associated (1 - ζ ^ j) (1 - ζ ^ k)
Tactic:
exact (this hj).symm.trans (this hk)
Proof state after:
no goals
Theorem: IsCyclotomicExtension.CyclotomicUnit.associated_one_sub_pow_primitive_root_of_coprime
Proof state before:
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
⊢ 1 - ζ ^ j = (1 - ζ) * ∑ i ∈ range j, ζ ^ i
Tactic:
rw [← geom_sum_mul_neg, mul_comm]
Proof state after:
no goals
Theorem: IsCyclotomicExtension.CyclotomicUnit.associated_one_sub_pow_primitive_root_of_coprime
Proof state before:
case inl
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
ζ : A
j : ℕ
hζ : IsPrimitiveRoot ζ 0
hj : j.Coprime 0
⊢ 1 - ζ ^ j ∣ 1 - ζ
Tactic:
simp [j.coprime_zero_right.mp hj]
Proof state after:
no goals
Theorem: IsCyclotomicExtension.CyclotomicUnit.associated_one_sub_pow_primitive_root_of_coprime
Proof state before:
case inr.inl
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
ζ : A
j : ℕ
hζ : IsPrimitiveRoot ζ 1
hj : j.Coprime 1
hn' : 1 ≠ 0
⊢ 1 - ζ ^ j ∣ 1 - ζ
Tactic:
simp [IsPrimitiveRoot.one_right_iff.mp hζ]
Proof state after:
no goals
Theorem: IsCyclotomicExtension.CyclotomicUnit.associated_one_sub_pow_primitive_root_of_coprime
Proof state before:
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : 1 < n
m : ℕ
hm : j * m % n = 1
⊢ ζ = (ζ ^ j) ^ m
Tactic:
rw [← pow_mul, ←pow_mod_orderOf, ← hζ.eq_orderOf, hm, pow_one]
Proof state after:
no goals
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit
Proof state before:
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
⊢ IsUnit (∑ i ∈ range k, ζ ^ i)
Tactic:
have h1 : (1 : ℕ).Coprime n := Nat.coprime_one_left n
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
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
⊢ IsUnit (∑ i ∈ range k, ζ ^ i)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit
Proof state before:
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
⊢ IsUnit (∑ i ∈ range k, ζ ^ i)
Tactic:
have := associated_one_sub_pow_primitive_root_of_coprime _ hζ hk h1
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
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
this : Associated (1 - ζ ^ 1) (1 - ζ ^ k)
⊢ IsUnit (∑ i ∈ range k, ζ ^ i)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit
Proof state before:
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
this : Associated (1 - ζ ^ 1) (1 - ζ ^ k)
⊢ IsUnit (∑ i ∈ range k, ζ ^ i)
Tactic:
simp at this
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
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
this : Associated (1 - ζ) (1 - ζ ^ k)
⊢ IsUnit (∑ i ∈ range k, ζ ^ i)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit
Proof state before:
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
this : Associated (1 - ζ) (1 - ζ ^ k)
⊢ IsUnit (∑ i ∈ range k, ζ ^ i)
Tactic:
rw [Associated] at this
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
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
this : ∃ u, (1 - ζ) * ↑u = 1 - ζ ^ k
⊢ IsUnit (∑ i ∈ range k, ζ ^ i)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit
Proof state before:
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
this : ∃ u, (1 - ζ) * ↑u = 1 - ζ ^ k
⊢ IsUnit (∑ i ∈ range k, ζ ^ i)
Tactic:
have h2 := mul_neg_geom_sum ζ k
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
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
this : ∃ u, (1 - ζ) * ↑u = 1 - ζ ^ k
h2 : (1 - ζ) * ∑ i ∈ range k, ζ ^ i = 1 - ζ ^ k
⊢ IsUnit (∑ i ∈ range k, ζ ^ i)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit
Proof state before:
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
this : ∃ u, (1 - ζ) * ↑u = 1 - ζ ^ k
h2 : (1 - ζ) * ∑ i ∈ range k, ζ ^ i = 1 - ζ ^ k
⊢ IsUnit (∑ i ∈ range k, ζ ^ i)
Tactic:
obtain ⟨u, hu⟩ := this
Proof state after:
case 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
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
h2 : (1 - ζ) * ∑ i ∈ range k, ζ ^ i = 1 - ζ ^ k
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
⊢ IsUnit (∑ i ∈ range k, ζ ^ i)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit
Proof state before:
case 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
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
h2 : (1 - ζ) * ∑ i ∈ range k, ζ ^ i = 1 - ζ ^ k
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
⊢ IsUnit (∑ i ∈ range k, ζ ^ i)
Tactic:
have := u.isUnit
Proof state after:
case 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
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
h2 : (1 - ζ) * ∑ i ∈ range k, ζ ^ i = 1 - ζ ^ k
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
⊢ IsUnit (∑ i ∈ range k, ζ ^ i)
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit
Proof state before:
case 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
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
h2 : (1 - ζ) * ∑ i ∈ range k, ζ ^ i = 1 - ζ ^ k
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
⊢ IsUnit (∑ i ∈ range k, ζ ^ i)
Tactic:
convert this
Proof state after:
case h.e'_3
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
h2 : (1 - ζ) * ∑ i ∈ range k, ζ ^ i = 1 - ζ ^ k
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
⊢ ∑ i ∈ range k, ζ ^ i = ↑u
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit
Proof state before:
case h.e'_3
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
h2 : (1 - ζ) * ∑ i ∈ range k, ζ ^ i = 1 - ζ ^ k
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
⊢ ∑ i ∈ range k, ζ ^ i = ↑u
Tactic:
rw [← hu] at h2
Proof state after:
case h.e'_3
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
u : Aˣ
h2 : (1 - ζ) * ∑ i ∈ range k, ζ ^ i = (1 - ζ) * ↑u
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
⊢ ∑ i ∈ range k, ζ ^ i = ↑u
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit
Proof state before:
case h.e'_3
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
u : Aˣ
h2 : (1 - ζ) * ∑ i ∈ range k, ζ ^ i = (1 - ζ) * ↑u
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
⊢ ∑ i ∈ range k, ζ ^ i = ↑u
Tactic:
simp at h2
Proof state after:
case h.e'_3
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
h2 : ∑ i ∈ range k, ζ ^ i = ↑u ∨ 1 - ζ = 0
⊢ ∑ i ∈ range k, ζ ^ i = ↑u
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit
Proof state before:
case h.e'_3
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
h2 : ∑ i ∈ range k, ζ ^ i = ↑u ∨ 1 - ζ = 0
⊢ ∑ i ∈ range k, ζ ^ i = ↑u
Tactic:
cases' h2 with h2 h2
Proof state after:
case h.e'_3.inl
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
h2 : ∑ i ∈ range k, ζ ^ i = ↑u
⊢ ∑ i ∈ range k, ζ ^ i = ↑u

case h.e'_3.inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
h2 : 1 - ζ = 0
⊢ ∑ i ∈ range k, ζ ^ i = ↑u
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit
Proof state before:
case h.e'_3.inl
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
h2 : ∑ i ∈ range k, ζ ^ i = ↑u
⊢ ∑ i ∈ range k, ζ ^ i = ↑u

case h.e'_3.inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
h2 : 1 - ζ = 0
⊢ ∑ i ∈ range k, ζ ^ i = ↑u
Tactic:
exact h2
Proof state after:
case h.e'_3.inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
h2 : 1 - ζ = 0
⊢ ∑ i ∈ range k, ζ ^ i = ↑u
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit
Proof state before:
case h.e'_3.inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
h2 : 1 - ζ = 0
⊢ ∑ i ∈ range k, ζ ^ i = ↑u
Tactic:
exfalso
Proof state after:
case h.e'_3.inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
h2 : 1 - ζ = 0
⊢ False
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit
Proof state before:
case h.e'_3.inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
h2 : 1 - ζ = 0
⊢ False
Tactic:
have hn1 : 1 < n := by linarith
Proof state after:
case h.e'_3.inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
h2 : 1 - ζ = 0
hn1 : 1 < n
⊢ False
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit
Proof state before:
case h.e'_3.inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
h2 : 1 - ζ = 0
hn1 : 1 < n
⊢ False
Tactic:
have hp := IsPrimitiveRoot.pow_ne_one_of_pos_of_lt hζ one_pos hn1
Proof state after:
case h.e'_3.inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
h2 : 1 - ζ = 0
hn1 : 1 < n
hp : ζ ^ 1 ≠ 1
⊢ False
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit
Proof state before:
case h.e'_3.inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
h1 : Nat.Coprime 1 n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
this : IsUnit ↑u
h2 : 1 - ζ = 0
hn1 : 1 < n
hp : ζ ^ 1 ≠ 1
⊢ False
Tactic:
simp at *
Proof state after:
case h.e'_3.inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
h2 : 1 - ζ = 0
hn1 : 1 < n
h1 this : True
hp : ¬ζ = 1
⊢ False
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit
Proof state before:
case h.e'_3.inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
h2 : 1 - ζ = 0
hn1 : 1 < n
h1 this : True
hp : ¬ζ = 1
⊢ False
Tactic:
rw [sub_eq_zero] at h2
Proof state after:
case h.e'_3.inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
h2 : 1 = ζ
hn1 : 1 < n
h1 this : True
hp : ¬ζ = 1
⊢ False
Theorem: IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit
Proof state before:
case h.e'_3.inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
h2 : 1 = ζ
hn1 : 1 < n
h1 this : True
hp : ¬ζ = 1
⊢ False
Tactic:
rw [← h2] at hp
Proof state after:
case h.e'_3.inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n k : ℕ
ζ : A
hn : 2 ≤ n
hk : k.Coprime n
hζ : IsPrimitiveRoot ζ n
u : Aˣ
hu : (1 - ζ) * ↑u = 1 - ζ ^ k
h2 : 1 = ζ
hn1 : 1 < n
h1 this : True
hp : ¬1 = 1
⊢ False