Theorem: one_sub_zeta_prime (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
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
⊢ _root_.Prime (1 - η)
Tactic:
have h := 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
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h : IsPrimitiveRoot ↑η ↑p
⊢ _root_.Prime (1 - η)

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h : IsPrimitiveRoot ↑η ↑p
⊢ _root_.Prime (1 - η)
Tactic:
simpa using h.zeta_sub_one_prime'.neg
State after:
no goals