Theorem: IsPrimitiveRoot.sub_one_dvd_sub (FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean)

State before:
K : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p✝} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
hp✝ : p✝ ≠ 2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
η₁ : A
hη₁ : η₁ ∈ nthRootsFinset p A
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p A
⊢ ζ - 1 ∣ η₁ - η₂
Tactic:
by_cases h : η₁ = η₂
State after:
case pos
K : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p✝} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
hp✝ : p✝ ≠ 2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
η₁ : A
hη₁ : η₁ ∈ nthRootsFinset p A
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p A
h : η₁ = η₂
⊢ ζ - 1 ∣ η₁ - η₂

case neg
K : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p✝} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
hp✝ : p✝ ≠ 2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
η₁ : A
hη₁ : η₁ ∈ nthRootsFinset p A
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p A
h : ¬η₁ = η₂
⊢ ζ - 1 ∣ η₁ - η₂

State before:
case pos
K : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p✝} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
hp✝ : p✝ ≠ 2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
η₁ : A
hη₁ : η₁ ∈ nthRootsFinset p A
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p A
h : η₁ = η₂
⊢ ζ - 1 ∣ η₁ - η₂
Tactic:
rw [h, sub_self]
State after:
case pos
K : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p✝} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
hp✝ : p✝ ≠ 2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
η₁ : A
hη₁ : η₁ ∈ nthRootsFinset p A
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p A
h : η₁ = η₂
⊢ ζ - 1 ∣ 0

State before:
case pos
K : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p✝} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
hp✝ : p✝ ≠ 2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
η₁ : A
hη₁ : η₁ ∈ nthRootsFinset p A
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p A
h : η₁ = η₂
⊢ ζ - 1 ∣ 0
Tactic:
exact dvd_zero _
State after:
no goals

State before:
case neg
K : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p✝} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
hp✝ : p✝ ≠ 2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
η₁ : A
hη₁ : η₁ ∈ nthRootsFinset p A
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p A
h : ¬η₁ = η₂
⊢ ζ - 1 ∣ η₁ - η₂
Tactic:
exact (hζ.associated_sub_one hp hη₁ hη₂ h).dvd
State after:
no goals