Theorem: IsCyclotomicExtension.CyclotomicUnit.associated_one_sub_pow_primitive_root_of_coprime (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
n j k : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
hk : k.Coprime n
hj : j.Coprime n
⊢ Associated (1 - ζ ^ j) (1 - ζ ^ k)
Tactic:
suffices ∀ {j : ℕ}, j.Coprime n → Associated (1 - ζ) (1 - ζ ^ j) by
  exact (this hj).symm.trans (this hk)
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 j k : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
hk : k.Coprime n
hj : j.Coprime n
⊢ ∀ {j : ℕ}, j.Coprime n → Associated (1 - ζ) (1 - ζ ^ 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
n j k : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
hk : k.Coprime n
hj : j.Coprime n
⊢ ∀ {j : ℕ}, j.Coprime n → Associated (1 - ζ) (1 - ζ ^ j)
Tactic:
clear k j hk 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
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
⊢ ∀ {j : ℕ}, j.Coprime n → Associated (1 - ζ) (1 - ζ ^ 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
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
⊢ ∀ {j : ℕ}, j.Coprime n → Associated (1 - ζ) (1 - ζ ^ j)
Tactic:
intro j 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
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
⊢ Associated (1 - ζ) (1 - ζ ^ 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
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
⊢ Associated (1 - ζ) (1 - ζ ^ j)
Tactic:
refine' associated_of_dvd_dvd ⟨∑ i in range j, ζ ^ i, by rw [← geom_sum_mul_neg, mul_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
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
⊢ 1 - ζ ^ j ∣ 1 - ζ

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 - ζ
Tactic:
rcases eq_or_ne n 0 with (rfl | hn')
State after:
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 - ζ

case 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 : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
⊢ 1 - ζ ^ j ∣ 1 - ζ

State before:
case 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 : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
⊢ 1 - ζ ^ j ∣ 1 - ζ
Tactic:
rcases eq_or_ne n 1 with (rfl | hn)
State after:
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 - ζ

case inr.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 : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : n ≠ 1
⊢ 1 - ζ ^ j ∣ 1 - ζ

State before:
case inr.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 : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : n ≠ 1
⊢ 1 - ζ ^ j ∣ 1 - ζ
Tactic:
replace hn := Nat.one_lt_of_ne n hn' hn
State after:
case inr.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 : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : 1 < n
⊢ 1 - ζ ^ j ∣ 1 - ζ

State before:
case inr.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 : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : 1 < n
⊢ 1 - ζ ^ j ∣ 1 - ζ
Tactic:
obtain ⟨m, hm⟩ := Nat.exists_mul_emod_eq_one_of_coprime hj hn
State after:
case inr.inr.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 : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : 1 < n
m : ℕ
hm : j * m % n = 1
⊢ 1 - ζ ^ j ∣ 1 - ζ

State before:
case inr.inr.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 : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : 1 < n
m : ℕ
hm : j * m % n = 1
⊢ 1 - ζ ^ j ∣ 1 - ζ
Tactic:
use ∑ i in range m, (ζ ^ j) ^ i
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
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : 1 < n
m : ℕ
hm : j * m % n = 1
⊢ 1 - ζ = (1 - ζ ^ j) * ∑ i ∈ range m, (ζ ^ j) ^ i

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
⊢ 1 - ζ = (1 - ζ ^ j) * ∑ i ∈ range m, (ζ ^ j) ^ i
Tactic:
have : ζ = (ζ ^ j) ^ m := by rw [← pow_mul, ←pow_mod_orderOf, ← hζ.eq_orderOf, hm, pow_one]
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
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 - ζ = (1 - ζ ^ j) * ∑ i ∈ range m, (ζ ^ j) ^ i

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 - ζ = (1 - ζ ^ j) * ∑ i ∈ range m, (ζ ^ j) ^ i
Tactic:
nth_rw 1 [this]
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
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

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

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

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