internlm/Lean-Github huggingface dataset:
Theorem: prod_c
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
e' : Ideal.span {∏ ζ ∈ nthRootsFinset (↑p) (𝓞 K), (x + ζ * y)} = (𝔭 ^ (m + 1) * 𝔷) ^ ↑p
⊢ ∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, 𝔠 η = (𝔷' * 𝔭 ^ m) ^ ↑p
Tactic:
rw [← Ideal.prod_span_singleton, ← Finset.prod_attach] at e'
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
e' : ∏ x_1 ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, Ideal.span {x + ↑x_1 * y} = (𝔭 ^ (m + 1) * 𝔷) ^ ↑p
⊢ ∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, 𝔠 η = (𝔷' * 𝔭 ^ m) ^ ↑p
Theorem: prod_c
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
e' : ∏ x_1 ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, Ideal.span {x + ↑x_1 * y} = (𝔭 ^ (m + 1) * 𝔷) ^ ↑p
⊢ ∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, 𝔠 η = (𝔷' * 𝔭 ^ m) ^ ↑p
Tactic:
simp_rw [mul_comm _ y, ← m_mul_c_mul_p hp hζ e hy,
  Finset.prod_mul_distrib, Finset.prod_const, Finset.card_attach,
  hζ.unit'_coe.card_nthRootsFinset] at e'
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
e' : (𝔪 ^ ↑p * ∏ x_1 ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, 𝔠 x_1) * 𝔭 ^ ↑p = (𝔭 ^ (m + 1) * 𝔷) ^ ↑p
⊢ ∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, 𝔠 η = (𝔷' * 𝔭 ^ m) ^ ↑p
Theorem: prod_c
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
e' : (𝔪 ^ ↑p * ∏ x_1 ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, 𝔠 x_1) * 𝔭 ^ ↑p = (𝔭 ^ (m + 1) * 𝔷) ^ ↑p
⊢ ∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach, 𝔠 η = (𝔷' * 𝔭 ^ m) ^ ↑p
Tactic:
rw [← mul_right_inj'
  ((pow_ne_zero_iff hpri.out.ne_zero).mpr (m_ne_zero hζ e hy) : _),
  ← mul_left_inj' ((pow_ne_zero_iff hpri.out.ne_zero).mpr (p_ne_zero hζ) : _), e',
  exists_ideal_pow_eq_c_aux]
Proof state after:
no goals
Theorem: exists_ideal_pow_eq_c
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ ∃ I, 𝔠 η = I ^ ↑p
Tactic:
letI inst1 : @IsDomain (Ideal (𝓞 K)) CommSemiring.toSemiring := @Ideal.isDomain (𝓞 K) _ _
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
inst1 : IsDomain (Ideal (𝓞 K)) := Ideal.isDomain
⊢ ∃ I, 𝔠 η = I ^ ↑p
Theorem: exists_ideal_pow_eq_c
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
inst1 : IsDomain (Ideal (𝓞 K)) := Ideal.isDomain
⊢ ∃ I, 𝔠 η = I ^ ↑p
Tactic:
letI inst2 := @Ideal.instNormalizedGCDMonoid (𝓞 K) _ _
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
inst1 : IsDomain (Ideal (𝓞 K)) := Ideal.isDomain
inst2 : NormalizedGCDMonoid (Ideal (𝓞 K)) := Ideal.instNormalizedGCDMonoid
⊢ ∃ I, 𝔠 η = I ^ ↑p
Theorem: exists_ideal_pow_eq_c
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
inst1 : IsDomain (Ideal (𝓞 K)) := Ideal.isDomain
inst2 : NormalizedGCDMonoid (Ideal (𝓞 K)) := Ideal.instNormalizedGCDMonoid
⊢ ∃ I, 𝔠 η = I ^ ↑p
Tactic:
letI inst3 := @NormalizedGCDMonoid.toGCDMonoid _ _ inst2
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
inst1 : IsDomain (Ideal (𝓞 K)) := Ideal.isDomain
inst2 : NormalizedGCDMonoid (Ideal (𝓞 K)) := Ideal.instNormalizedGCDMonoid
inst3 : GCDMonoid (Ideal (𝓞 K)) := NormalizedGCDMonoid.toGCDMonoid
⊢ ∃ I, 𝔠 η = I ^ ↑p
Theorem: exists_ideal_pow_eq_c
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
inst1 : IsDomain (Ideal (𝓞 K)) := Ideal.isDomain
inst2 : NormalizedGCDMonoid (Ideal (𝓞 K)) := Ideal.instNormalizedGCDMonoid
inst3 : GCDMonoid (Ideal (𝓞 K)) := NormalizedGCDMonoid.toGCDMonoid
⊢ ∃ I, 𝔠 η = I ^ ↑p
Tactic:
exact @Finset.exists_eq_pow_of_mul_eq_pow_of_coprime (nthRootsFinset p (𝓞 K)) (Ideal (𝓞 K)) _
  (by convert inst1) (by convert inst3) _ _ _ _ _
  (λ η₁ _ η₂ _ hη ↦ coprime_c hp hζ e hy η₁ η₂ hη)
  (prod_c hp hζ e hy) η (Finset.mem_attach _ _)
Proof state after:
no goals
Theorem: exists_ideal_pow_eq_c
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
inst1 : IsDomain (Ideal (𝓞 K)) := Ideal.isDomain
inst2 : NormalizedGCDMonoid (Ideal (𝓞 K)) := Ideal.instNormalizedGCDMonoid
inst3 : GCDMonoid (Ideal (𝓞 K)) := NormalizedGCDMonoid.toGCDMonoid
⊢ IsDomain (Ideal (𝓞 K))
Tactic:
convert inst1
Proof state after:
no goals
Theorem: exists_ideal_pow_eq_c
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
inst1 : IsDomain (Ideal (𝓞 K)) := Ideal.isDomain
inst2 : NormalizedGCDMonoid (Ideal (𝓞 K)) := Ideal.instNormalizedGCDMonoid
inst3 : GCDMonoid (Ideal (𝓞 K)) := NormalizedGCDMonoid.toGCDMonoid
⊢ GCDMonoid (Ideal (𝓞 K))
Tactic:
convert inst3
Proof state after:
no goals
Theorem: c_div_principal_aux
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ ↑(𝔦↑η₁) / ↑(𝔦↑η₂) = ↑(𝔠 η₁) / ↑(𝔠 η₂)
Tactic:
simp_rw [← m_mul_c_mul_p hp hζ e hy, FractionalIdeal.coeIdeal_mul]
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ ↑𝔪 * ↑(𝔠 η₁) * ↑𝔭 / (↑𝔪 * ↑(𝔠 η₂) * ↑𝔭) = ↑(𝔠 η₁) / ↑(𝔠 η₂)
Theorem: c_div_principal_aux
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ ↑𝔪 * ↑(𝔠 η₁) * ↑𝔭 / (↑𝔪 * ↑(𝔠 η₂) * ↑𝔭) = ↑(𝔠 η₁) / ↑(𝔠 η₂)
Tactic:
rw [mul_div_mul_right, mul_div_mul_left]
Proof state after:
case hc
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ ↑𝔪 ≠ 0

case hc
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ ↑𝔭 ≠ 0
Theorem: c_div_principal_aux
Proof state before:
case hc
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ ↑𝔪 ≠ 0
Tactic:
rw [← FractionalIdeal.coeIdeal_bot, (FractionalIdeal.coeIdeal_injective' le_rfl).ne_iff]
Proof state after:
case hc
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ 𝔪 ≠ ⊥
Theorem: c_div_principal_aux
Proof state before:
case hc
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ 𝔪 ≠ ⊥
Tactic:
exact m_ne_zero hζ e hy
Proof state after:
no goals
Theorem: c_div_principal_aux
Proof state before:
case hc
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ ↑𝔭 ≠ 0
Tactic:
rw [← FractionalIdeal.coeIdeal_bot, (FractionalIdeal.coeIdeal_injective' le_rfl).ne_iff]
Proof state after:
case hc
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ 𝔭 ≠ ⊥
Theorem: c_div_principal_aux
Proof state before:
case hc
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ 𝔭 ≠ ⊥
Tactic:
exact p_ne_zero hζ
Proof state after:
no goals
Theorem: c_div_principal
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ (↑(↑(𝔠 η₁) / ↑(𝔠 η₂))).IsPrincipal
Tactic:
rw [← c_div_principal_aux, FractionalIdeal.coeIdeal_span_singleton,
  FractionalIdeal.coeIdeal_span_singleton, FractionalIdeal.spanSingleton_div_spanSingleton,
  FractionalIdeal.coe_spanSingleton]
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ (Submodule.span (𝓞 K) {(algebraMap (𝓞 K) K) (x + y * ↑η₁) / (algebraMap (𝓞 K) K) (x + y * ↑η₂)}).IsPrincipal
Theorem: c_div_principal
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ (Submodule.span (𝓞 K) {(algebraMap (𝓞 K) K) (x + y * ↑η₁) / (algebraMap (𝓞 K) K) (x + y * ↑η₂)}).IsPrincipal
Tactic:
exact ⟨⟨_, rfl⟩⟩
Proof state after:
no goals
Theorem: a_div_principal
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ (↑(↑(𝔞 η₁) / ↑(𝔞 η₂))).IsPrincipal
Tactic:
apply isPrincipal_of_isPrincipal_pow_of_Coprime' _ hreg
Proof state after:
case hI
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ (↑((↑(𝔞 η₁) / ↑(𝔞 η₂)) ^ ↑p)).IsPrincipal
Theorem: a_div_principal
Proof state before:
case hI
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ (↑((↑(𝔞 η₁) / ↑(𝔞 η₂)) ^ ↑p)).IsPrincipal
Tactic:
rw [div_pow, ← FractionalIdeal.coeIdeal_pow, ← FractionalIdeal.coeIdeal_pow,
  root_div_zeta_sub_one_dvd_gcd_spec, root_div_zeta_sub_one_dvd_gcd_spec]
Proof state after:
case hI
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ (↑(↑(𝔠 η₁) / ↑(𝔠 η₂))).IsPrincipal
Theorem: a_div_principal
Proof state before:
case hI
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ (↑(↑(𝔠 η₁) / ↑(𝔠 η₂))).IsPrincipal
Tactic:
exact c_div_principal hp hζ e hy η₁ η₂
Proof state after:
no goals
Theorem: p_dvd_c_iff
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ 𝔭 ∣ 𝔠 η ↔ η = η₀
Tactic:
rw [← (div_zeta_sub_one_Injective hp hζ e hy).eq_iff, zeta_sub_one_dvd_root_spec,
  Ideal.Quotient.eq_zero_iff_dvd, ← Ideal.mem_span_singleton (α := 𝓞 K),
  ← Ideal.dvd_span_singleton, ← div_zeta_sub_one_dvd_gcd_spec (hy := hy),
  ← dvd_gcd_mul_iff_dvd_mul, gcd_comm, gcd_zeta_sub_one_eq_one hζ hy, one_mul]
Proof state after:
no goals
Theorem: p_pow_dvd_c_eta_zero_aux
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝¹ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
inst✝ : DecidableEq (𝓞 K)
⊢ gcd (𝔭 ^ (m * ↑p)) (∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach \ {η₀}, 𝔠 η) = 1
Tactic:
rw [← Ideal.isCoprime_iff_gcd]
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝¹ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
inst✝ : DecidableEq (𝓞 K)
⊢ IsCoprime (𝔭 ^ (m * ↑p)) (∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach \ {η₀}, 𝔠 η)
Theorem: p_pow_dvd_c_eta_zero_aux
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝¹ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
inst✝ : DecidableEq (𝓞 K)
⊢ IsCoprime (𝔭 ^ (m * ↑p)) (∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach \ {η₀}, 𝔠 η)
Tactic:
apply IsCoprime.pow_left
Proof state after:
case H
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝¹ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
inst✝ : DecidableEq (𝓞 K)
⊢ IsCoprime 𝔭 (∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach \ {η₀}, 𝔠 η)
Theorem: p_pow_dvd_c_eta_zero_aux
Proof state before:
case H
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝¹ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
inst✝ : DecidableEq (𝓞 K)
⊢ IsCoprime 𝔭 (∏ η ∈ (nthRootsFinset (↑p) (𝓞 K)).attach \ {η₀}, 𝔠 η)
Tactic:
rw [Ideal.isCoprime_iff_gcd, hζ.prime_span_sub_one.irreducible.gcd_eq_one_iff,
  hζ.prime_span_sub_one.dvd_finset_prod_iff]
Proof state after:
case H
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝¹ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
inst✝ : DecidableEq (𝓞 K)
⊢ ¬∃ a ∈ (nthRootsFinset (↑p) (𝓞 K)).attach \ {η₀}, 𝔭 ∣ 𝔠 a