internlm/Lean-Github huggingface dataset:
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) = 1 - η
Tactic:
ring
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
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
⊢ IsPrimitiveRoot ↑η ↑p
Tactic:
apply prim_coe η (nth_roots_prim hη hne1)
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
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
⊢ p ≠ 2
Tactic:
intro hP
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
hP : p = 2
⊢ False
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
hP : p = 2
⊢ False
Tactic:
rw [hP] at ph
Proof 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
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 ≤ 2
η : 𝓞 (CyclotomicField p ℚ)
hη : η ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hne1 : η ≠ 1
h00 : 1 - η ∣ ↑↑p ↔ η - 1 ∣ ↑↑p
this : IsPrimitiveRoot ↑η ↑p
hP : p = 2
⊢ False
Tactic:
contradiction
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
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
Proof state after:
no goals
Theorem: one_sub_zeta_prime
Proof 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)
Proof 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 - η)
Theorem: one_sub_zeta_prime
Proof 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
Proof state after:
no goals
Theorem: diff_of_roots
Proof state before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
ph : 5 ≤ p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)
Tactic:
replace ph : 2 ≤ p := le_trans (by decide) ph
Proof state after:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)
Theorem: diff_of_roots
Proof state before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)
Tactic:
have h := nth_roots_prim hη₁ hwlog
Proof state after:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)
Theorem: diff_of_roots
Proof state before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)
Tactic:
obtain ⟨i, ⟨H, hi⟩⟩ := h.eq_pow_of_pow_eq_one ((mem_nthRootsFinset hp.out.pos).1 hη₂) hp.out.pos
Proof state after:
case intro.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)
Theorem: diff_of_roots
Proof state before:
case intro.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)
Tactic:
have hi1 : 1 ≠ i := by
  intro hi1
  rw [← hi1, pow_one] at hi
  exact hdiff hi
Proof state after:
case intro.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
hi1 : 1 ≠ i
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)
Theorem: diff_of_roots
Proof state before:
case intro.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
hi1 : 1 ≠ i
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)
Tactic:
obtain ⟨u, hu⟩ :=
  CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one R ph hp.out hp.out.one_lt H
    hi1 h
Proof state after:
case intro.intro.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
hi1 : 1 ≠ i
u : (𝓞 (CyclotomicField p ℚ))ˣ
hu : η₁ ^ 1 - η₁ ^ i = ↑u * (1 - η₁)
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)
Theorem: diff_of_roots
Proof state before:
case intro.intro.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
hi1 : 1 ≠ i
u : (𝓞 (CyclotomicField p ℚ))ˣ
hu : η₁ ^ 1 - η₁ ^ i = ↑u * (1 - η₁)
⊢ ∃ u, η₁ - η₂ = ↑u * (1 - η₁)
Tactic:
refine' ⟨u, _⟩
Proof state after:
case intro.intro.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
hi1 : 1 ≠ i
u : (𝓞 (CyclotomicField p ℚ))ˣ
hu : η₁ ^ 1 - η₁ ^ i = ↑u * (1 - η₁)
⊢ η₁ - η₂ = ↑u * (1 - η₁)
Theorem: diff_of_roots
Proof state before:
case intro.intro.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
hi1 : 1 ≠ i
u : (𝓞 (CyclotomicField p ℚ))ˣ
hu : η₁ ^ 1 - η₁ ^ i = ↑u * (1 - η₁)
⊢ η₁ - η₂ = ↑u * (1 - η₁)
Tactic:
rw [← hu, hi, pow_one]
Proof state after:
no goals
Theorem: diff_of_roots
Proof state before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
ph : 5 ≤ p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
⊢ 2 ≤ 5
Tactic:
decide
Proof state after:
no goals
Theorem: diff_of_roots
Proof state before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
⊢ 1 ≠ i
Tactic:
intro hi1
Proof state after:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
hi1 : 1 = i
⊢ False
Theorem: diff_of_roots
Proof state before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ ^ i = η₂
hi1 : 1 = i
⊢ False
Tactic:
rw [← hi1, pow_one] at hi
Proof state after:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ = η₂
hi1 : 1 = i
⊢ False
Theorem: diff_of_roots
Proof state before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
ph : 2 ≤ p
h : IsPrimitiveRoot η₁ ↑p
i : ℕ
H : i < ↑p
hi : η₁ = η₂
hi1 : 1 = i
⊢ False
Tactic:
exact hdiff hi
Proof state after:
no goals
Theorem: diff_of_roots2
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 ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
⊢ ∃ u, η₂ - η₁ = ↑u * (1 - η₁)
Tactic:
obtain ⟨u, hu⟩ := diff_of_roots ph hη₁ hη₂ hdiff hwlog
Proof state after:
case intro
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 ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
u : (𝓞 (CyclotomicField p ℚ))ˣ
hu : η₁ - η₂ = ↑u * (1 - η₁)
⊢ ∃ u, η₂ - η₁ = ↑u * (1 - η₁)
Theorem: diff_of_roots2
Proof state before:
case intro
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 ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
u : (𝓞 (CyclotomicField p ℚ))ˣ
hu : η₁ - η₂ = ↑u * (1 - η₁)
⊢ ∃ u, η₂ - η₁ = ↑u * (1 - η₁)
Tactic:
refine' ⟨-u, _⟩
Proof state after:
case intro
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 ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
u : (𝓞 (CyclotomicField p ℚ))ˣ
hu : η₁ - η₂ = ↑u * (1 - η₁)
⊢ η₂ - η₁ = ↑(-u) * (1 - η₁)
Theorem: diff_of_roots2
Proof state before:
case intro
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 ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
u : (𝓞 (CyclotomicField p ℚ))ˣ
hu : η₁ - η₂ = ↑u * (1 - η₁)
⊢ η₂ - η₁ = ↑(-u) * (1 - η₁)
Tactic:
rw [Units.val_neg, neg_mul, ← hu]
Proof state after:
case intro
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 ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
u : (𝓞 (CyclotomicField p ℚ))ˣ
hu : η₁ - η₂ = ↑u * (1 - η₁)
⊢ η₂ - η₁ = -(η₁ - η₂)
Theorem: diff_of_roots2
Proof state before:
case intro
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 ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
u : (𝓞 (CyclotomicField p ℚ))ˣ
hu : η₁ - η₂ = ↑u * (1 - η₁)
⊢ η₂ - η₁ = -(η₁ - η₂)
Tactic:
ring
Proof state after:
no goals
Theorem: fltIdeals_coprime2_lemma
Proof state before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
⊢ fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤
Tactic:
apply by_contradiction
Proof state after:
case a
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
⊢ ¬fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤ → False
Theorem: fltIdeals_coprime2_lemma
Proof state before:
case a
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
⊢ ¬fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤ → False
Tactic:
intro h
Proof state after:
case a
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
h : ¬fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤
⊢ False
Theorem: fltIdeals_coprime2_lemma
Proof state before:
case a
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
h : ¬fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤
⊢ False
Tactic:
let I := fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂
Proof state after:
case a
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
h : ¬fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤
I : Ideal (𝓞 (CyclotomicField p ℚ)) := fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂
⊢ False
Theorem: fltIdeals_coprime2_lemma
Proof state before:
case a
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
h : ¬fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤
I : Ideal (𝓞 (CyclotomicField p ℚ)) := fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂
⊢ False
Tactic:
obtain ⟨P, hP1, hP2⟩ := exists_le_maximal I h
Proof state after:
case a.intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
h : ¬fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤
I : Ideal (𝓞 (CyclotomicField p ℚ)) := fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂
P : Ideal (𝓞 (CyclotomicField p ℚ))
hP1 : P.IsMaximal
hP2 : I ≤ P
⊢ False
Theorem: fltIdeals_coprime2_lemma
Proof state before:
case a.intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
h : ¬fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤
I : Ideal (𝓞 (CyclotomicField p ℚ)) := fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂
P : Ideal (𝓞 (CyclotomicField p ℚ))
hP1 : P.IsMaximal
hP2 : I ≤ P
⊢ False
Tactic:
have hiP : fltIdeals p x y hη₁ ≤ P := le_trans le_sup_left hP2
Proof state after:
case a.intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
h : ¬fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤
I : Ideal (𝓞 (CyclotomicField p ℚ)) := fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂
P : Ideal (𝓞 (CyclotomicField p ℚ))
hP1 : P.IsMaximal
hP2 : I ≤ P
hiP : fltIdeals p x y hη₁ ≤ P
⊢ False
Theorem: fltIdeals_coprime2_lemma
Proof state before:
case a.intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
h : ¬fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤
I : Ideal (𝓞 (CyclotomicField p ℚ)) := fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂
P : Ideal (𝓞 (CyclotomicField p ℚ))
hP1 : P.IsMaximal
hP2 : I ≤ P
hiP : fltIdeals p x y hη₁ ≤ P
⊢ False
Tactic:
have hel1 : ∃ v : Rˣ, (v : R) * y * (1 - η₁) ∈ I := by
  obtain ⟨v, hv⟩ := diff_of_roots ph hη₁ hη₂ hdiff hwlog
  refine ⟨v, ?_⟩
  have := Ideal.sub_mem _
    (mem_sup_left (mem_fltIdeals x y hη₁)) (mem_sup_right (mem_fltIdeals x y hη₂))
  rwa [add_sub_add_left_eq_sub, ← sub_mul, hv, mul_right_comm] at this
Proof state after:
case a.intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
h : ¬fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤
I : Ideal (𝓞 (CyclotomicField p ℚ)) := fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂
P : Ideal (𝓞 (CyclotomicField p ℚ))
hP1 : P.IsMaximal
hP2 : I ≤ P
hiP : fltIdeals p x y hη₁ ≤ P
hel1 : ∃ v, ↑v * ↑y * (1 - η₁) ∈ I
⊢ False