internlm/Lean-Github huggingface dataset:
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
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
⊢ {1 - η₁} ⊆ ↑P
Tactic:
simp [h]
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
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
⊢ comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P = span {↑↑p}
Tactic:
have H1 : Ideal.span ({(p : ℤ)} : Set ℤ) ≤ P.comap (Int.castRingHom R) := by
  rw [← hηP]
  apply le_comap_of_map_le _
  rw [map_span]
  simp
  rw [span_singleton_le_span_singleton]
  apply zeta_sub_one_dvb_p ph hη₁ hwlog
Proof state after:
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
H1 : span {↑↑p} ≤ comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P
⊢ comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P = span {↑↑p}
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
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
H1 : span {↑↑p} ≤ comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P
⊢ comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P = span {↑↑p}
Tactic:
have H2 : IsPrime (P.comap (Int.castRingHom R)) := by
  exact IsPrime.comap _
Proof state after:
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
H1 : span {↑↑p} ≤ comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P
H2 : (comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P).IsPrime
⊢ comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P = span {↑↑p}
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
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
H1 : span {↑↑p} ≤ comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P
H2 : (comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P).IsPrime
⊢ comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P = span {↑↑p}
Tactic:
have H4 : Ideal.span ({(p : ℤ)} : Set ℤ) ≠ ⊥ := by simp
Proof state after:
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
H1 : span {↑↑p} ≤ comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P
H2 : (comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P).IsPrime
H4 : span {↑↑p} ≠ ⊥
⊢ comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P = span {↑↑p}
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
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
H1 : span {↑↑p} ≤ comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P
H2 : (comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P).IsPrime
H4 : span {↑↑p} ≠ ⊥
⊢ comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P = span {↑↑p}
Tactic:
apply ((@Ring.DimensionLeOne.prime_le_prime_iff_eq _ _ _ _ _ H5 H2 H4).1 H1).symm
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
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
⊢ span {↑↑p} ≤ comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P
Tactic:
rw [← hηP]
Proof state after:
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
⊢ span {↑↑p} ≤ comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) (span {1 - η₁})
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
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
⊢ span {↑↑p} ≤ comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) (span {1 - η₁})
Tactic:
apply le_comap_of_map_le _
Proof state after:
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
⊢ Ideal.map (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) (span {↑↑p}) ≤ span {1 - η₁}
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
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
⊢ Ideal.map (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) (span {↑↑p}) ≤ span {1 - η₁}
Tactic:
rw [map_span]
Proof state after:
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
⊢ span (⇑(Int.castRingHom (𝓞 (CyclotomicField p ℚ))) '' {↑↑p}) ≤ span {1 - η₁}
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
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
⊢ span (⇑(Int.castRingHom (𝓞 (CyclotomicField p ℚ))) '' {↑↑p}) ≤ span {1 - η₁}
Tactic:
simp
Proof state after:
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
⊢ span {↑↑p} ≤ span {1 - η₁}
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
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
⊢ span {↑↑p} ≤ span {1 - η₁}
Tactic:
rw [span_singleton_le_span_singleton]
Proof state after:
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
⊢ 1 - η₁ ∣ ↑↑p
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
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
⊢ 1 - η₁ ∣ ↑↑p
Tactic:
apply zeta_sub_one_dvb_p ph hη₁ hwlog
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
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
H1 : span {↑↑p} ≤ comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P
⊢ (comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P).IsPrime
Tactic:
exact IsPrime.comap _
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
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
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
H1 : span {↑↑p} ≤ comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P
H2 : (comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P).IsPrime
⊢ span {↑↑p} ≠ ⊥
Tactic:
simp
Proof state after:
no goals