Theorem: IsPrimitiveRoot.associated_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
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
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 - η₂)

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

State before:
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)
Tactic:
have : i ≠ j := ne_of_apply_ne _ e
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
this : i ≠ j
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)

State before:
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
this : i ≠ j
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)
Tactic:
obtain ⟨u, h⟩ := IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one A
  hp.two_le hp hi hj this hζ
State after:
case intro.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
this : i ≠ j
u : Aˣ
h : ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)

State before:
case intro.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
this : i ≠ j
u : Aˣ
h : ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)
Tactic:
rw [h, associated_isUnit_mul_right_iff u.isUnit, ← associated_isUnit_mul_right_iff isUnit_one.neg,
  neg_one_mul, neg_sub]
State after:
case intro.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
this : i ≠ j
u : Aˣ
h : ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
⊢ Associated (ζ - 1) (ζ - 1)

State before:
case intro.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
this : i ≠ j
u : Aˣ
h : ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
⊢ Associated (ζ - 1) (ζ - 1)
Tactic:
rfl
State after:
no goals