Theorem: nth_roots_prim (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
⊢ IsPrimitiveRoot η ↑p
Tactic:
have hζ' := (zeta_spec p ℚ (CyclotomicField p ℚ)).unit'_coe
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 ↑⋯.unit' ↑p
⊢ IsPrimitiveRoot η ↑p

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 ↑⋯.unit' ↑p
⊢ IsPrimitiveRoot η ↑p
Tactic:
rw [nthRoots_one_eq_biUnion_primitiveRoots' hζ'] at hη
State after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ (↑p).divisors.biUnion fun i => primitiveRoots i (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
⊢ IsPrimitiveRoot η ↑p

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ (↑p).divisors.biUnion fun i => primitiveRoots i (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
⊢ IsPrimitiveRoot η ↑p
Tactic:
simp only [mem_biUnion] at hη
State after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
hη : ∃ a ∈ (↑p).divisors, η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
⊢ IsPrimitiveRoot η ↑p

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
hη : ∃ a ∈ (↑p).divisors, η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
⊢ IsPrimitiveRoot η ↑p
Tactic:
obtain ⟨a, ha, h2⟩ := hη
State after:
case intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
ha : a ∈ (↑p).divisors
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
⊢ IsPrimitiveRoot η ↑p

State before:
case intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
ha : a ∈ (↑p).divisors
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
⊢ IsPrimitiveRoot η ↑p
Tactic:
have ha2 : a = p := by
  rw [Nat.Prime.divisors (Fact.out : Nat.Prime p), mem_insert, mem_singleton] at ha
  cases' ha with ha ha
  exfalso
  rw [ha] at h2
  simp at h2
  rw [h2] at hne1
  exact hne1 rfl
  exact ha
State after:
case intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
ha : a ∈ (↑p).divisors
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
ha2 : a = ↑p
⊢ IsPrimitiveRoot η ↑p

State before:
case intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
ha : a ∈ (↑p).divisors
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
ha2 : a = ↑p
⊢ IsPrimitiveRoot η ↑p
Tactic:
rw [ha2] at h2
State after:
case intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
ha : a ∈ (↑p).divisors
h2 : η ∈ primitiveRoots (↑p) (𝓞 (CyclotomicField p ℚ))
ha2 : a = ↑p
⊢ IsPrimitiveRoot η ↑p

State before:
case intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
ha : a ∈ (↑p).divisors
h2 : η ∈ primitiveRoots (↑p) (𝓞 (CyclotomicField p ℚ))
ha2 : a = ↑p
⊢ IsPrimitiveRoot η ↑p
Tactic:
have hn : 0 < (p : ℕ) := by norm_num
State after:
case intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
ha : a ∈ (↑p).divisors
h2 : η ∈ primitiveRoots (↑p) (𝓞 (CyclotomicField p ℚ))
ha2 : a = ↑p
hn : 0 < ↑p
⊢ IsPrimitiveRoot η ↑p

State before:
case intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
ha : a ∈ (↑p).divisors
h2 : η ∈ primitiveRoots (↑p) (𝓞 (CyclotomicField p ℚ))
ha2 : a = ↑p
hn : 0 < ↑p
⊢ IsPrimitiveRoot η ↑p
Tactic:
rw [mem_primitiveRoots hn] at h2
State after:
case intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
ha : a ∈ (↑p).divisors
h2 : IsPrimitiveRoot η ↑p
ha2 : a = ↑p
hn : 0 < ↑p
⊢ IsPrimitiveRoot η ↑p

State before:
case intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
ha : a ∈ (↑p).divisors
h2 : IsPrimitiveRoot η ↑p
ha2 : a = ↑p
hn : 0 < ↑p
⊢ IsPrimitiveRoot η ↑p
Tactic:
exact h2
State after:
no goals

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
ha : a ∈ (↑p).divisors
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
⊢ a = ↑p
Tactic:
rw [Nat.Prime.divisors (Fact.out : Nat.Prime p), mem_insert, mem_singleton] at ha
State after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
ha : a = 1 ∨ a = ↑p
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
⊢ a = ↑p

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
ha : a = 1 ∨ a = ↑p
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
⊢ a = ↑p
Tactic:
cases' ha with ha ha
State after:
case inl
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
ha : a = 1
⊢ a = ↑p

case inr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
ha : a = ↑p
⊢ a = ↑p

State before:
case inl
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
ha : a = 1
⊢ a = ↑p

case inr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
ha : a = ↑p
⊢ a = ↑p
Tactic:
exfalso
State after:
case inl
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
ha : a = 1
⊢ False

case inr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
ha : a = ↑p
⊢ a = ↑p

State before:
case inl
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
ha : a = 1
⊢ False

case inr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
ha : a = ↑p
⊢ a = ↑p
Tactic:
rw [ha] at h2
State after:
case inl
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
h2 : η ∈ primitiveRoots 1 (𝓞 (CyclotomicField p ℚ))
ha : a = 1
⊢ False

case inr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
ha : a = ↑p
⊢ a = ↑p

State before:
case inl
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
h2 : η ∈ primitiveRoots 1 (𝓞 (CyclotomicField p ℚ))
ha : a = 1
⊢ False

case inr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
ha : a = ↑p
⊢ a = ↑p
Tactic:
simp at h2
State after:
case inl
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
ha : a = 1
h2 : η = 1
⊢ False

case inr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
ha : a = ↑p
⊢ a = ↑p

State before:
case inl
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
ha : a = 1
h2 : η = 1
⊢ False

case inr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
ha : a = ↑p
⊢ a = ↑p
Tactic:
rw [h2] at hne1
State after:
case inl
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : 1 ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
ha : a = 1
h2 : η = 1
⊢ False

case inr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
ha : a = ↑p
⊢ a = ↑p

State before:
case inl
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : 1 ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
ha : a = 1
h2 : η = 1
⊢ False

case inr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
ha : a = ↑p
⊢ a = ↑p
Tactic:
exact hne1 rfl
State after:
case inr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
ha : a = ↑p
⊢ a = ↑p

State before:
case inr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
h2 : η ∈ primitiveRoots a (𝓞 (CyclotomicField p ℚ))
ha : a = ↑p
⊢ a = ↑p
Tactic:
exact ha
State after:
no goals

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
η : 𝓞 (CyclotomicField p ℚ)
hne1 : η ≠ 1
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑p
a : ℕ
ha : a ∈ (↑p).divisors
h2 : η ∈ primitiveRoots (↑p) (𝓞 (CyclotomicField p ℚ))
ha2 : a = ↑p
⊢ 0 < ↑p
Tactic:
norm_num
State after:
no goals