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

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
⊢ 1 - η ∣ ↑↑p
Tactic:
have h00 : 1 - η ∣ (p : R) ↔ η - 1 ∣ (p : R) :=  by
  have hh : -(η - 1) = 1 - η := by ring
  simp_rw [← hh]
  apply neg_dvd
State after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
⊢ 1 - η ∣ ↑↑p

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
⊢ 1 - η ∣ ↑↑p
Tactic:
rw [h00]
State after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
⊢ η - 1 ∣ ↑↑p

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
⊢ η - 1 ∣ ↑↑p
Tactic:
have : IsPrimitiveRoot (η : CyclotomicField p ℚ) p := by
  apply prim_coe η (nth_roots_prim hη hne1)
State after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
⊢ η - 1 ∣ ↑↑p

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
⊢ η - 1 ∣ ↑↑p
Tactic:
have h0 : p ≠ 2 := by
  intro hP
  rw [hP] at ph
  contradiction
State after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
h0 : p ≠ 2
⊢ η - 1 ∣ ↑↑p

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
h0 : p ≠ 2
⊢ η - 1 ∣ ↑↑p
Tactic:
have h := RingOfIntegers.dvd_norm ℚ (η - 1 : R)
State after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
h0 : p ≠ 2
h : η - 1 ∣ (algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField p ℚ))) ((RingOfIntegers.norm ℚ) (η - 1))
⊢ η - 1 ∣ ↑↑p

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
h0 : p ≠ 2
h : η - 1 ∣ (algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField p ℚ))) ((RingOfIntegers.norm ℚ) (η - 1))
⊢ η - 1 ∣ ↑↑p
Tactic:
have h2 := IsPrimitiveRoot.norm_sub_one_of_prime_ne_two' this (cyclotomic.irreducible_rat p.2) h0
State after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
h0 : p ≠ 2
h : η - 1 ∣ (algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField p ℚ))) ((RingOfIntegers.norm ℚ) (η - 1))
h2 : (Algebra.norm ℚ) (↑η - 1) = ↑↑p
⊢ η - 1 ∣ ↑↑p

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
h0 : p ≠ 2
h : η - 1 ∣ (algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField p ℚ))) ((RingOfIntegers.norm ℚ) (η - 1))
h2 : (Algebra.norm ℚ) (↑η - 1) = ↑↑p
⊢ η - 1 ∣ ↑↑p
Tactic:
convert h
State after:
case h.e'_4
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
h0 : p ≠ 2
h : η - 1 ∣ (algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField p ℚ))) ((RingOfIntegers.norm ℚ) (η - 1))
h2 : (Algebra.norm ℚ) (↑η - 1) = ↑↑p
⊢ ↑↑p = (algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField p ℚ))) ((RingOfIntegers.norm ℚ) (η - 1))

State before:
case h.e'_4
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
h0 : p ≠ 2
h : η - 1 ∣ (algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField p ℚ))) ((RingOfIntegers.norm ℚ) (η - 1))
h2 : (Algebra.norm ℚ) (↑η - 1) = ↑↑p
⊢ ↑↑p = (algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField p ℚ))) ((RingOfIntegers.norm ℚ) (η - 1))
Tactic:
ext
State after:
case h.e'_4.h
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
h0 : p ≠ 2
h : η - 1 ∣ (algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField p ℚ))) ((RingOfIntegers.norm ℚ) (η - 1))
h2 : (Algebra.norm ℚ) (↑η - 1) = ↑↑p
⊢ ↑↑↑p = ↑((algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField p ℚ))) ((RingOfIntegers.norm ℚ) (η - 1)))

State before:
case h.e'_4.h
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
h0 : p ≠ 2
h : η - 1 ∣ (algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField p ℚ))) ((RingOfIntegers.norm ℚ) (η - 1))
h2 : (Algebra.norm ℚ) (↑η - 1) = ↑↑p
⊢ ↑↑↑p = ↑((algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField p ℚ))) ((RingOfIntegers.norm ℚ) (η - 1)))
Tactic:
rw [show (η : CyclotomicField p ℚ) - 1 = (η - 1 : _) by simp] at h2
State after:
case h.e'_4.h
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
h0 : p ≠ 2
h : η - 1 ∣ (algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField p ℚ))) ((RingOfIntegers.norm ℚ) (η - 1))
h2 : (Algebra.norm ℚ) ↑(η - 1) = ↑↑p
⊢ ↑↑↑p = ↑((algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField p ℚ))) ((RingOfIntegers.norm ℚ) (η - 1)))

State before:
case h.e'_4.h
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
h0 : p ≠ 2
h : η - 1 ∣ (algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField p ℚ))) ((RingOfIntegers.norm ℚ) (η - 1))
h2 : (Algebra.norm ℚ) ↑(η - 1) = ↑↑p
⊢ ↑↑↑p = ↑((algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField p ℚ))) ((RingOfIntegers.norm ℚ) (η - 1)))
Tactic:
rw [RingOfIntegers.coe_algebraMap_norm, h2]
State after:
case h.e'_4.h
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
h0 : p ≠ 2
h : η - 1 ∣ (algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField p ℚ))) ((RingOfIntegers.norm ℚ) (η - 1))
h2 : (Algebra.norm ℚ) ↑(η - 1) = ↑↑p
⊢ ↑↑↑p = (algebraMap ℚ (CyclotomicField p ℚ)) ↑↑p

State before:
case h.e'_4.h
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
h0 : p ≠ 2
h : η - 1 ∣ (algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField p ℚ))) ((RingOfIntegers.norm ℚ) (η - 1))
h2 : (Algebra.norm ℚ) ↑(η - 1) = ↑↑p
⊢ ↑↑↑p = (algebraMap ℚ (CyclotomicField p ℚ)) ↑↑p
Tactic:
simp
State after:
no goals

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
⊢ 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
Tactic:
have hh : -(η - 1) = 1 - η := by ring
State after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
hh : -(η - 1) = 1 - η
⊢ 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
hh : -(η - 1) = 1 - η
⊢ 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
Tactic:
simp_rw [← hh]
State after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
hh : -(η - 1) = 1 - η
⊢ -(η - 1) ∣ ↑↑p ↔ η - 1 ∣ ↑↑p

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
hh : -(η - 1) = 1 - η
⊢ -(η - 1) ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
Tactic:
apply neg_dvd
State after:
no goals

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
⊢ -(η - 1) = 1 - η
Tactic:
ring
State after:
no goals

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
⊢ IsPrimitiveRoot ↑η ↑p
Tactic:
apply prim_coe η (nth_roots_prim hη hne1)
State after:
no goals

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
⊢ p ≠ 2
Tactic:
intro hP
State after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
hP : p = 2
⊢ False

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
hP : p = 2
⊢ False
Tactic:
rw [hP] at ph
State after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ 2
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
hP : p = 2
⊢ False

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ 2
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
hP : p = 2
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
h0 : p ≠ 2
h : η - 1 ∣ (algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField p ℚ))) ((RingOfIntegers.norm ℚ) (η - 1))
h2 : (Algebra.norm ℚ) (↑η - 1) = ↑↑p
⊢ ↑η - 1 = ↑(η - 1)
Tactic:
simp
State after:
no goals