internlm/Lean-Github huggingface dataset:
Theorem: div_zeta_sub_one_sub
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) }
hη : η₁ ≠ η₂
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Associated (y * π) ((div_zeta_sub_one hp hζ e η₁ - div_zeta_sub_one hp hζ e η₂) * π)
Tactic:
convert_to Associated _ (y * (η₁ - η₂))
Proof state after:
case h.e'_4
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) }
hη : η₁ ≠ η₂
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ (div_zeta_sub_one hp hζ e η₁ - div_zeta_sub_one hp hζ e η₂) * π = y * (↑η₁ - ↑η₂)

case convert_2
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) }
hη : η₁ ≠ η₂
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Associated (y * π) (y * (↑η₁ - ↑η₂))
Theorem: div_zeta_sub_one_sub
Proof state before:
case convert_2
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) }
hη : η₁ ≠ η₂
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Associated (y * π) (y * (↑η₁ - ↑η₂))
Tactic:
apply Associated.mul_left
Proof state after:
case convert_2.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) }
hη : η₁ ≠ η₂
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Associated π (↑η₁ - ↑η₂)
Theorem: div_zeta_sub_one_sub
Proof state before:
case convert_2.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) }
hη : η₁ ≠ η₂
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Associated π (↑η₁ - ↑η₂)
Tactic:
apply hζ.unit'_coe.associated_sub_one hpri.out η₁.prop η₂.prop
Proof state after:
case convert_2.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) }
hη : η₁ ≠ η₂
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ ↑η₁ ≠ ↑η₂
Theorem: div_zeta_sub_one_sub
Proof state before:
case convert_2.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) }
hη : η₁ ≠ η₂
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ ↑η₁ ≠ ↑η₂
Tactic:
rw [Ne, ← Subtype.ext_iff.not]
Proof state after:
case convert_2.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) }
hη : η₁ ≠ η₂
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ ¬η₁ = η₂
Theorem: div_zeta_sub_one_sub
Proof state before:
case convert_2.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) }
hη : η₁ ≠ η₂
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ ¬η₁ = η₂
Tactic:
exact hη
Proof state after:
no goals
Theorem: div_zeta_sub_one_sub
Proof state before:
case h.e'_4
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) }
hη : η₁ ≠ η₂
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ (div_zeta_sub_one hp hζ e η₁ - div_zeta_sub_one hp hζ e η₂) * π = y * (↑η₁ - ↑η₂)
Tactic:
rw [sub_mul, div_zeta_sub_one_mul_zeta_sub_one, div_zeta_sub_one_mul_zeta_sub_one]
Proof state after:
case h.e'_4
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) }
hη : η₁ ≠ η₂
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ x + y * ↑η₁ - (x + y * ↑η₂) = y * (↑η₁ - ↑η₂)
Theorem: div_zeta_sub_one_sub
Proof state before:
case h.e'_4
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) }
hη : η₁ ≠ η₂
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ x + y * ↑η₁ - (x + y * ↑η₂) = y * (↑η₁ - ↑η₂)
Tactic:
ring
Proof state after:
no goals
Theorem: div_zeta_sub_one_Injective
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) }
⊢ Function.Injective fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)
Tactic:
letI : AddGroup (𝓞 K ⧸ 𝔭) := inferInstance
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) }
this : AddGroup (𝓞 K ⧸ 𝔭) := inferInstance
⊢ Function.Injective fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)
Theorem: div_zeta_sub_one_Injective
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) }
this : AddGroup (𝓞 K ⧸ 𝔭) := inferInstance
⊢ Function.Injective fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)
Tactic:
intros η₁ η₂
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) }
this : AddGroup (𝓞 K ⧸ 𝔭) := inferInstance
η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ (fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)) η₁ =
      (fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)) η₂ →
    η₁ = η₂
Theorem: div_zeta_sub_one_Injective
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) }
this : AddGroup (𝓞 K ⧸ 𝔭) := inferInstance
η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ (fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)) η₁ =
      (fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)) η₂ →
    η₁ = η₂
Tactic:
contrapose
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) }
this : AddGroup (𝓞 K ⧸ 𝔭) := inferInstance
η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ ¬η₁ = η₂ →
    ¬(fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)) η₁ =
        (fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)) η₂
Theorem: div_zeta_sub_one_Injective
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) }
this : AddGroup (𝓞 K ⧸ 𝔭) := inferInstance
η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ ¬η₁ = η₂ →
    ¬(fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)) η₁ =
        (fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)) η₂
Tactic:
intro e₁ 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) }
this : AddGroup (𝓞 K ⧸ 𝔭) := inferInstance
η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
e₁ : ¬η₁ = η₂
e₂ :
  (fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)) η₁ =
    (fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)) η₂
⊢ False
Theorem: div_zeta_sub_one_Injective
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) }
this : AddGroup (𝓞 K ⧸ 𝔭) := inferInstance
η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
e₁ : ¬η₁ = η₂
e₂ :
  (fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)) η₁ =
    (fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)) η₂
⊢ False
Tactic:
apply hy
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) }
this : AddGroup (𝓞 K ⧸ 𝔭) := inferInstance
η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
e₁ : ¬η₁ = η₂
e₂ :
  (fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)) η₁ =
    (fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)) η₂
⊢ π ∣ y
Theorem: div_zeta_sub_one_Injective
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) }
this : AddGroup (𝓞 K ⧸ 𝔭) := inferInstance
η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
e₁ : ¬η₁ = η₂
e₂ :
  (fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)) η₁ =
    (fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)) η₂
⊢ π ∣ y
Tactic:
obtain ⟨u, e⟩ := div_zeta_sub_one_sub hp hζ e η₁ η₂ e₁
Proof state after:
case intro
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) }
this : AddGroup (𝓞 K ⧸ 𝔭) := inferInstance
η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
e₁ : ¬η₁ = η₂
e₂ :
  (fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e✝ η)) η₁ =
    (fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e✝ η)) η₂
u : (𝓞 K)ˣ
e : y * ↑u = div_zeta_sub_one hp hζ e✝ η₁ - div_zeta_sub_one hp hζ e✝ η₂
⊢ π ∣ y
Theorem: div_zeta_sub_one_Injective
Proof state before:
case intro
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) }
this : AddGroup (𝓞 K ⧸ 𝔭) := inferInstance
η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
e₁ : ¬η₁ = η₂
e₂ :
  (fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e✝ η)) η₁ =
    (fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e✝ η)) η₂
u : (𝓞 K)ˣ
e : y * ↑u = div_zeta_sub_one hp hζ e✝ η₁ - div_zeta_sub_one hp hζ e✝ η₂
⊢ π ∣ y
Tactic:
dsimp only at e₂
Proof state after:
case intro
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) }
this : AddGroup (𝓞 K ⧸ 𝔭) := inferInstance
η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
e₁ : ¬η₁ = η₂
e₂ : (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e✝ η₁) = (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e✝ η₂)
u : (𝓞 K)ˣ
e : y * ↑u = div_zeta_sub_one hp hζ e✝ η₁ - div_zeta_sub_one hp hζ e✝ η₂
⊢ π ∣ y
Theorem: div_zeta_sub_one_Injective
Proof state before:
case intro
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) }
this : AddGroup (𝓞 K ⧸ 𝔭) := inferInstance
η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
e₁ : ¬η₁ = η₂
e₂ : (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e✝ η₁) = (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e✝ η₂)
u : (𝓞 K)ˣ
e : y * ↑u = div_zeta_sub_one hp hζ e✝ η₁ - div_zeta_sub_one hp hζ e✝ η₂
⊢ π ∣ y
Tactic:
rwa [← sub_eq_zero, ← map_sub, ← e, Ideal.Quotient.eq_zero_iff_dvd, u.isUnit.dvd_mul_right] at e₂
Proof state after:
no goals
Theorem: div_zeta_sub_one_Bijective
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) }
⊢ Function.Bijective fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)
Tactic:
haveI : Fact (Nat.Prime p) := hpri
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) }
this : Fact (↑p).Prime
⊢ Function.Bijective fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)
Theorem: div_zeta_sub_one_Bijective
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) }
this : Fact (↑p).Prime
⊢ Function.Bijective fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)
Tactic:
letI := Fintype.ofFinite (𝓞 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) }
this✝ : Fact (↑p).Prime
this : Fintype (𝓞 K ⧸ 𝔭) := Fintype.ofFinite (𝓞 K ⧸ 𝔭)
⊢ Function.Bijective fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)
Theorem: div_zeta_sub_one_Bijective
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) }
this✝ : Fact (↑p).Prime
this : Fintype (𝓞 K ⧸ 𝔭) := Fintype.ofFinite (𝓞 K ⧸ 𝔭)
⊢ Function.Bijective fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)
Tactic:
letI := IsCyclotomicExtension.numberField {p} ℚ 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) }
this✝¹ : Fact (↑p).Prime
this✝ : Fintype (𝓞 K ⧸ 𝔭) := Fintype.ofFinite (𝓞 K ⧸ 𝔭)
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Function.Bijective fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)
Theorem: div_zeta_sub_one_Bijective
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) }
this✝¹ : Fact (↑p).Prime
this✝ : Fintype (𝓞 K ⧸ 𝔭) := Fintype.ofFinite (𝓞 K ⧸ 𝔭)
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Function.Bijective fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)
Tactic:
rw [Fintype.bijective_iff_injective_and_card]
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) }
this✝¹ : Fact (↑p).Prime
this✝ : Fintype (𝓞 K ⧸ 𝔭) := Fintype.ofFinite (𝓞 K ⧸ 𝔭)
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ (Function.Injective fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)) ∧
    Fintype.card { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } = Fintype.card (𝓞 K ⧸ 𝔭)