internlm/Lean-Github huggingface dataset:
Theorem: quotient_zero_sub_one_comp_aut
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ = Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})
Tactic:
apply RingHom.toIntAlgHom_injective
Proof state after:
case a
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ((Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ).toIntAlgHom =
    (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).toIntAlgHom
Theorem: quotient_zero_sub_one_comp_aut
Proof state before:
case a
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ((Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ).toIntAlgHom =
    (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).toIntAlgHom
Tactic:
apply hζ.integralPowerBasis'.algHom_ext
Proof state after:
case a.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ((Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ).toIntAlgHom hζ.integralPowerBasis'.gen =
    (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).toIntAlgHom hζ.integralPowerBasis'.gen
Theorem: quotient_zero_sub_one_comp_aut
Proof state before:
case a.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ((Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ).toIntAlgHom hζ.integralPowerBasis'.gen =
    (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).toIntAlgHom hζ.integralPowerBasis'.gen
Tactic:
rw [show hζ.integralPowerBasis'.gen = hζ.unit' from Subtype.ext (by simp)]
Proof state after:
case a.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ((Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ).toIntAlgHom ↑hζ.unit' =
    (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).toIntAlgHom ↑hζ.unit'
Theorem: quotient_zero_sub_one_comp_aut
Proof state before:
case a.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ((Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).comp σ).toIntAlgHom ↑hζ.unit' =
    (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})).toIntAlgHom ↑hζ.unit'
Tactic:
simp only [RingHom.toIntAlgHom, RingHom.toMonoidHom_eq_coe, AlgHom.coe_mk, RingHom.coe_mk,
  MonoidHom.coe_coe, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply]
Proof state after:
case a.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})) (σ ↑hζ.unit') =
    (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})) ↑hζ.unit'
Theorem: quotient_zero_sub_one_comp_aut
Proof state before:
case a.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})) (σ ↑hζ.unit') =
    (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})) ↑hζ.unit'
Tactic:
rw [← sub_eq_zero, ← map_sub, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]
Proof state after:
case a.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ↑hζ.unit' - 1 ∣ σ ↑hζ.unit' - ↑hζ.unit'
Theorem: quotient_zero_sub_one_comp_aut
Proof state before:
case a.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ↑hζ.unit' - 1 ∣ σ ↑hζ.unit' - ↑hζ.unit'
Tactic:
apply hζ.unit'_coe.sub_one_dvd_sub hpri.out
Proof state after:
case a.h.hη₁
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ σ ↑hζ.unit' ∈ nthRootsFinset (↑p) (𝓞 K)

case a.h.hη₂
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ↑hζ.unit' ∈ nthRootsFinset (↑p) (𝓞 K)
Theorem: quotient_zero_sub_one_comp_aut
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ↑hζ.integralPowerBasis'.gen = ↑↑hζ.unit'
Tactic:
simp
Proof state after:
no goals
Theorem: quotient_zero_sub_one_comp_aut
Proof state before:
case a.h.hη₁
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ σ ↑hζ.unit' ∈ nthRootsFinset (↑p) (𝓞 K)
Tactic:
rw [mem_nthRootsFinset p.pos, ← map_pow, hζ.unit'_coe.pow_eq_one, map_one]
Proof state after:
no goals
Theorem: quotient_zero_sub_one_comp_aut
Proof state before:
case a.h.hη₂
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
σ : 𝓞 K →+* 𝓞 K
this✝¹ : Fact (↑p).Prime
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : AddGroup (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}) := inferInstance
⊢ ↑hζ.unit' ∈ nthRootsFinset (↑p) (𝓞 K)
Tactic:
rw [mem_nthRootsFinset p.pos, hζ.unit'_coe.pow_eq_one]
Proof state after:
no goals
Theorem: zeta_sub_one_dvd_trace_sub_smul
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
⊢ ↑hζ.unit' - 1 ∣ ↑((Algebra.trace ℤ (𝓞 K)) x) - (↑p - 1) • x
Tactic:
letI := IsCyclotomicExtension.numberField {p} ℚ K
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ ↑hζ.unit' - 1 ∣ ↑((Algebra.trace ℤ (𝓞 K)) x) - (↑p - 1) • x
Theorem: zeta_sub_one_dvd_trace_sub_smul
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ ↑hζ.unit' - 1 ∣ ↑((Algebra.trace ℤ (𝓞 K)) x) - (↑p - 1) • x
Tactic:
letI := IsCyclotomicExtension.isGalois p ℚ K
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : IsGalois ℚ K := IsCyclotomicExtension.isGalois p ℚ K
⊢ ↑hζ.unit' - 1 ∣ ↑((Algebra.trace ℤ (𝓞 K)) x) - (↑p - 1) • x
Theorem: zeta_sub_one_dvd_trace_sub_smul
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : IsGalois ℚ K := IsCyclotomicExtension.isGalois p ℚ K
⊢ ↑hζ.unit' - 1 ∣ ↑((Algebra.trace ℤ (𝓞 K)) x) - (↑p - 1) • x
Tactic:
have : (Algebra.trace ℤ _ x : 𝓞 K) = ∑ σ : K ≃ₐ[ℚ] K, (intGal σ).toRingHom x := by
  apply (show Function.Injective (algebraMap (𝓞 K) K) from Subtype.val_injective)
  rw [← eq_intCast (algebraMap ℤ (𝓞 K)), ← IsScalarTower.algebraMap_apply,
    IsScalarTower.algebraMap_apply ℤ ℚ K, eq_intCast, Algebra.coe_trace_int,
    trace_eq_sum_automorphisms, map_sum]
  rfl
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this✝¹ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this✝ : IsGalois ℚ K := IsCyclotomicExtension.isGalois p ℚ K
this : ↑((Algebra.trace ℤ (𝓞 K)) x) = ∑ σ : K ≃ₐ[ℚ] K, (intGal ↑σ).toRingHom x
⊢ ↑hζ.unit' - 1 ∣ ↑((Algebra.trace ℤ (𝓞 K)) x) - (↑p - 1) • x
Theorem: zeta_sub_one_dvd_trace_sub_smul
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this✝¹ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this✝ : IsGalois ℚ K := IsCyclotomicExtension.isGalois p ℚ K
this : ↑((Algebra.trace ℤ (𝓞 K)) x) = ∑ σ : K ≃ₐ[ℚ] K, (intGal ↑σ).toRingHom x
⊢ ↑hζ.unit' - 1 ∣ ↑((Algebra.trace ℤ (𝓞 K)) x) - (↑p - 1) • x
Tactic:
rw [← Ideal.mem_span_singleton, ← Ideal.Quotient.eq_zero_iff_mem, map_sub, this,
  map_sum]
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this✝¹ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this✝ : IsGalois ℚ K := IsCyclotomicExtension.isGalois p ℚ K
this : ↑((Algebra.trace ℤ (𝓞 K)) x) = ∑ σ : K ≃ₐ[ℚ] K, (intGal ↑σ).toRingHom x
⊢ ∑ x_1 : K ≃ₐ[ℚ] K, (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})) ((intGal ↑x_1).toRingHom x) -
      (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})) ((↑p - 1) • x) =
    0
Theorem: zeta_sub_one_dvd_trace_sub_smul
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this✝¹ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this✝ : IsGalois ℚ K := IsCyclotomicExtension.isGalois p ℚ K
this : ↑((Algebra.trace ℤ (𝓞 K)) x) = ∑ σ : K ≃ₐ[ℚ] K, (intGal ↑σ).toRingHom x
⊢ ∑ x_1 : K ≃ₐ[ℚ] K, (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})) ((intGal ↑x_1).toRingHom x) -
      (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})) ((↑p - 1) • x) =
    0
Tactic:
simp_rw [← RingHom.comp_apply, quotient_zero_sub_one_comp_aut]
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this✝¹ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this✝ : IsGalois ℚ K := IsCyclotomicExtension.isGalois p ℚ K
this : ↑((Algebra.trace ℤ (𝓞 K)) x) = ∑ σ : K ≃ₐ[ℚ] K, (intGal ↑σ).toRingHom x
⊢ ∑ x_1 : K ≃ₐ[ℚ] K, (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})) x -
      (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})) ((↑p - 1) • x) =
    0
Theorem: zeta_sub_one_dvd_trace_sub_smul
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this✝¹ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this✝ : IsGalois ℚ K := IsCyclotomicExtension.isGalois p ℚ K
this : ↑((Algebra.trace ℤ (𝓞 K)) x) = ∑ σ : K ≃ₐ[ℚ] K, (intGal ↑σ).toRingHom x
⊢ ∑ x_1 : K ≃ₐ[ℚ] K, (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})) x -
      (Ideal.Quotient.mk (Ideal.span {↑hζ.unit' - 1})) ((↑p - 1) • x) =
    0
Tactic:
rw [Finset.sum_const, map_nsmul, sub_eq_zero, Finset.card_univ, IsGalois.card_aut_eq_finrank,
  IsCyclotomicExtension.finrank K (cyclotomic.irreducible_rat p.pos), Nat.totient_prime hpri.out]
Proof state after:
no goals
Theorem: zeta_sub_one_dvd_trace_sub_smul
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : IsGalois ℚ K := IsCyclotomicExtension.isGalois p ℚ K
⊢ ↑((Algebra.trace ℤ (𝓞 K)) x) = ∑ σ : K ≃ₐ[ℚ] K, (intGal ↑σ).toRingHom x
Tactic:
apply (show Function.Injective (algebraMap (𝓞 K) K) from Subtype.val_injective)
Proof state after:
case a
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : IsGalois ℚ K := IsCyclotomicExtension.isGalois p ℚ K
⊢ (algebraMap (𝓞 K) K) ↑((Algebra.trace ℤ (𝓞 K)) x) = (algebraMap (𝓞 K) K) (∑ σ : K ≃ₐ[ℚ] K, (intGal ↑σ).toRingHom x)
Theorem: zeta_sub_one_dvd_trace_sub_smul
Proof state before:
case a
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : IsGalois ℚ K := IsCyclotomicExtension.isGalois p ℚ K
⊢ (algebraMap (𝓞 K) K) ↑((Algebra.trace ℤ (𝓞 K)) x) = (algebraMap (𝓞 K) K) (∑ σ : K ≃ₐ[ℚ] K, (intGal ↑σ).toRingHom x)
Tactic:
rw [← eq_intCast (algebraMap ℤ (𝓞 K)), ← IsScalarTower.algebraMap_apply,
  IsScalarTower.algebraMap_apply ℤ ℚ K, eq_intCast, Algebra.coe_trace_int,
  trace_eq_sum_automorphisms, map_sum]
Proof state after:
case a
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : IsGalois ℚ K := IsCyclotomicExtension.isGalois p ℚ K
⊢ ∑ σ : K ≃ₐ[ℚ] K, σ ↑x = ∑ x_1 : K ≃ₐ[ℚ] K, (algebraMap (𝓞 K) K) ((intGal ↑x_1).toRingHom x)
Theorem: zeta_sub_one_dvd_trace_sub_smul
Proof state before:
case a
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : IsGalois ℚ K := IsCyclotomicExtension.isGalois p ℚ K
⊢ ∑ σ : K ≃ₐ[ℚ] K, σ ↑x = ∑ x_1 : K ≃ₐ[ℚ] K, (algebraMap (𝓞 K) K) ((intGal ↑x_1).toRingHom x)
Tactic:
rfl
Proof state after:
no goals
Theorem: zeta_sub_one_pow_dvd_norm_sub_pow
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x
Tactic:
letI := IsCyclotomicExtension.numberField {p} ℚ K
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x
Theorem: zeta_sub_one_pow_dvd_norm_sub_pow
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x
Tactic:
obtain ⟨r, hr⟩ := Algebra.norm_one_add_smul (p : ℤ) x
Proof state after:
case intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x
Theorem: zeta_sub_one_pow_dvd_norm_sub_pow
Proof state before:
case intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x
Tactic:
obtain ⟨s, hs⟩ := zeta_sub_one_dvd_trace_sub_smul hζ x
Proof state after:
case intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) - (↑p - 1) • x = (↑hζ.unit' - 1) * s
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x
Theorem: zeta_sub_one_pow_dvd_norm_sub_pow
Proof state before:
case intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) - (↑p - 1) • x = (↑hζ.unit' - 1) * s
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x
Tactic:
obtain ⟨t, ht⟩ := (associated_zeta_sub_one_pow_prime hζ).dvd
Proof state after:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) - (↑p - 1) • x = (↑hζ.unit' - 1) * s
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x
Theorem: zeta_sub_one_pow_dvd_norm_sub_pow
Proof state before:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) - (↑p - 1) • x = (↑hζ.unit' - 1) * s
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x
Tactic:
rw [sub_eq_iff_eq_add] at hs
Proof state after:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x
Theorem: zeta_sub_one_pow_dvd_norm_sub_pow
Proof state before:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x
Tactic:
simp only [zsmul_eq_mul, Int.cast_natCast] at hr
Proof state after:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x