Theorem: diff_of_roots (FltRegular/NumberTheory/Cyclotomic/CyclRat.lean)

State before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
ph : 5 ≤ p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)
Tactic:
replace ph : 2 ≤ p := le_trans (by decide) ph
State after:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)

State before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)
Tactic:
have h := nth_roots_prim hη₁ hwlog
State after:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)

State before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)
Tactic:
obtain ⟨i, ⟨H, hi⟩⟩ := h.eq_pow_of_pow_eq_one ((mem_nthRootsFinset hp.out.pos).1 hη₂) hp.out.pos
State after:
case intro.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)

State before:
case intro.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)
Tactic:
have hi1 : 1 ≠ i := by
  intro hi1
  rw [← hi1, pow_one] at hi
  exact hdiff hi
State after:
case intro.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
hi1 : 1 ≠ i
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)

State before:
case intro.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
hi1 : 1 ≠ i
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)
Tactic:
obtain ⟨u, hu⟩ :=
  CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one R ph hp.out hp.out.one_lt H
    hi1 h
State after:
case intro.intro.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
hi1 : 1 ≠ i
u : (𝓞 (CyclotomicField p ℚ))ˣ
hu : η₁ ^ 1 - η₁ ^ i = ↑u * (1 - η₁)
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)

State before:
case intro.intro.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
hi1 : 1 ≠ i
u : (𝓞 (CyclotomicField p ℚ))ˣ
hu : η₁ ^ 1 - η₁ ^ i = ↑u * (1 - η₁)
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)
Tactic:
refine' ⟨u, _⟩
State after:
case intro.intro.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
hi1 : 1 ≠ i
u : (𝓞 (CyclotomicField p ℚ))ˣ
hu : η₁ ^ 1 - η₁ ^ i = ↑u * (1 - η₁)
⊢ η₁ - η₂ = ↑u * (1 - η₁)

State before:
case intro.intro.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
hi1 : 1 ≠ i
u : (𝓞 (CyclotomicField p ℚ))ˣ
hu : η₁ ^ 1 - η₁ ^ i = ↑u * (1 - η₁)
⊢ η₁ - η₂ = ↑u * (1 - η₁)
Tactic:
rw [← hu, hi, pow_one]
State after:
no goals

State before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
ph : 5 ≤ p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
⊢ 2 ≤ 5
Tactic:
decide
State after:
no goals

State before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
⊢ 1 ≠ i
Tactic:
intro hi1
State after:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
hi1 : 1 = i
⊢ False

State before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
hi1 : 1 = i
⊢ False
Tactic:
rw [← hi1, pow_one] at hi
State after:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ = η₂
hi1 : 1 = i
⊢ False

State before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ = η₂
hi1 : 1 = i
⊢ False
Tactic:
exact hdiff hi
State after:
no goals