have h2 := IsPrimitiveRoot.norm_sub_one_of_prime_ne_two' this (cyclotomic.irreducible_rat p.2) h0
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
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