internlm/Lean-Github huggingface dataset:
Theorem: nth_roots_prim
Proof 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η
Proof 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
Theorem: nth_roots_prim
Proof 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η
Proof 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
Theorem: nth_roots_prim
Proof 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
Proof 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
Theorem: nth_roots_prim
Proof 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
Proof 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
Theorem: nth_roots_prim
Proof 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
Proof 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
Theorem: nth_roots_prim
Proof 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
Proof 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
Theorem: nth_roots_prim
Proof 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
Proof state after:
no goals
Theorem: nth_roots_prim
Proof 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
Proof 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
Theorem: nth_roots_prim
Proof 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
Proof 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
Theorem: nth_roots_prim
Proof 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
Proof 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
Theorem: nth_roots_prim
Proof 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
Proof 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
Theorem: nth_roots_prim
Proof 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
Proof 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
Theorem: nth_roots_prim
Proof 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
Proof 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
Theorem: nth_roots_prim
Proof 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
Proof 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
Theorem: nth_roots_prim
Proof 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
Proof state after:
no goals
Theorem: nth_roots_prim
Proof 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
Proof state after:
no goals
Theorem: zeta_sub_one_dvb_p
Proof 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
Proof 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
Theorem: zeta_sub_one_dvb_p
Proof 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]
Proof 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
Theorem: zeta_sub_one_dvb_p
Proof 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)
Proof 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
Theorem: zeta_sub_one_dvb_p
Proof 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
Proof 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
Theorem: zeta_sub_one_dvb_p
Proof 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)
Proof 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
Theorem: zeta_sub_one_dvb_p
Proof 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
Proof 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
Theorem: zeta_sub_one_dvb_p
Proof 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
Proof 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))
Theorem: zeta_sub_one_dvb_p
Proof 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
Proof 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)))
Theorem: zeta_sub_one_dvb_p
Proof 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
Proof 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)))
Theorem: zeta_sub_one_dvb_p
Proof 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]
Proof 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
Theorem: zeta_sub_one_dvb_p
Proof 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
Proof state after:
no goals
Theorem: zeta_sub_one_dvb_p
Proof 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
Proof 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
Theorem: zeta_sub_one_dvb_p
Proof 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]
Proof 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
Theorem: zeta_sub_one_dvb_p
Proof 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
Proof state after:
no goals