internlm/Lean-Github huggingface dataset:
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
⊢ ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
Tactic:
refine' Eq.trans _ hu'
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
⊢ ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) =
    (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x)
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
⊢ ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) =
    (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x)
Tactic:
rw [map_sum]
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
⊢ ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) =
    ∑ x : Fin hζ.integralPowerBasis'.dim,
      (intGal ↑(galConj K p)) ((hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x)
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
⊢ ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) =
    ∑ x : Fin hζ.integralPowerBasis'.dim,
      (intGal ↑(galConj K p)) ((hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x)
Tactic:
congr 1
Proof state after:
case e_f
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
⊢ (fun x => (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x)) = fun x =>
    (intGal ↑(galConj K p)) ((hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x)
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof state before:
case e_f
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
⊢ (fun x => (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x)) = fun x =>
    (intGal ↑(galConj K p)) ((hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x)
Tactic:
ext x
Proof state after:
case e_f.h.h
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
x : Fin φn
⊢ ↑((a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x)) =
    ↑((intGal ↑(galConj K p)) ((hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x))
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof state before:
case e_f.h.h
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
x : Fin φn
⊢ ↑((a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x)) =
    ↑((intGal ↑(galConj K p)) ((hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x))
Tactic:
congr 1
Proof state after:
case e_f.h.h.e_x
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
x : Fin φn
⊢ (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) =
    (intGal ↑(galConj K p)) ((hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x)
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof state before:
case e_f.h.h.e_x
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
x : Fin φn
⊢ (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) =
    (intGal ↑(galConj K p)) ((hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x)
Tactic:
rw [map_zsmul]
Proof state after:
no goals
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
⊢ ∀ (x : Fin φn), (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ⟨ζ⁻¹, ⋯⟩ ^ ↑x
Tactic:
intro x
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
x : Fin φn
⊢ (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ⟨ζ⁻¹, ⋯⟩ ^ ↑x
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
x : Fin φn
⊢ (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ⟨ζ⁻¹, ⋯⟩ ^ ↑x
Tactic:
ext
Proof state after:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
x : Fin φn
⊢ ↑((intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x)) = ↑(⟨ζ⁻¹, ⋯⟩ ^ ↑x)
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof state before:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
x : Fin φn
⊢ ↑((intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x)) = ↑(⟨ζ⁻¹, ⋯⟩ ^ ↑x)
Tactic:
simp only [map_pow, intGal_apply_coe, RingOfIntegers.map_mk, AlgHom.coe_coe, inv_pow]
Proof state after:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
x : Fin φn
⊢ (galConj K p) ζ ^ ↑x = (ζ ^ ↑x)⁻¹
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof state before:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
x : Fin φn
⊢ (galConj K p) ζ ^ ↑x = (ζ ^ ↑x)⁻¹
Tactic:
rw [← map_pow, galConj_zeta_runity_pow hζ, inv_pow]
Proof state after:
no goals
Theorem: unit_inv_conj_not_neg_zeta_runity
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
⊢ u * ((unitGalConj K p) u)⁻¹ ≠ -hζ.unit' ^ n
Tactic:
by_contra H
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
⊢ False
Theorem: unit_inv_conj_not_neg_zeta_runity
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
⊢ False
Tactic:
have hμ : algebraMap (𝓞 K) (𝓞 K ⧸ I) ((IsPrimitiveRoot.unit' hζ : 𝓞 K) ^ n) = 1 := by
  apply hζ.unit'_coe.eq_one_mod_sub_of_pow
  rw [← pow_mul, mul_comm, pow_mul, hζ.unit'_coe.pow_eq_one, one_pow]
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
⊢ False
Theorem: unit_inv_conj_not_neg_zeta_runity
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
⊢ False
Tactic:
have hμ' : algebraMap (𝓞 K) (𝓞 K ⧸ I) ((IsPrimitiveRoot.unit' hζ : 𝓞 K) ^ n) = -1 := by
  rw [← neg_eq_iff_eq_neg, ← map_neg, ← Units.val_pow_eq_pow_val, ← Units.val_neg, ← H]
  apply unit_inv_conj_not_neg_zeta_runity_aux hζ u hp
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
hμ' : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = -1
⊢ False
Theorem: unit_inv_conj_not_neg_zeta_runity
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
hμ' : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = -1
⊢ False
Tactic:
haveI := Fact.mk hp
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
hμ' : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = -1
this : Fact (↑p).Prime
⊢ False
Theorem: unit_inv_conj_not_neg_zeta_runity
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
hμ' : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = -1
this : Fact (↑p).Prime
⊢ False
Tactic:
apply hζ.two_not_mem_one_sub_zeta h
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
hμ' : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = -1
this : Fact (↑p).Prime
⊢ 2 ∈ Ideal.span {↑hζ.unit' - 1}
Theorem: unit_inv_conj_not_neg_zeta_runity
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
hμ' : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = -1
this : Fact (↑p).Prime
⊢ 2 ∈ Ideal.span {↑hζ.unit' - 1}
Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem, map_two, ← neg_one_eq_one_iff_two_eq_zero, ← hμ', hμ]
Proof state after:
no goals
Theorem: unit_inv_conj_not_neg_zeta_runity
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
Tactic:
apply hζ.unit'_coe.eq_one_mod_sub_of_pow
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
⊢ (↑hζ.unit' ^ n) ^ ↑p = 1
Theorem: unit_inv_conj_not_neg_zeta_runity
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
⊢ (↑hζ.unit' ^ n) ^ ↑p = 1
Tactic:
rw [← pow_mul, mul_comm, pow_mul, hζ.unit'_coe.pow_eq_one, one_pow]
Proof state after:
no goals
Theorem: unit_inv_conj_not_neg_zeta_runity
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = -1
Tactic:
rw [← neg_eq_iff_eq_neg, ← map_neg, ← Units.val_pow_eq_pow_val, ← Units.val_neg, ← H]
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑(u * ((unitGalConj K p) u)⁻¹) = 1
Theorem: unit_inv_conj_not_neg_zeta_runity
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑(u * ((unitGalConj K p) u)⁻¹) = 1
Tactic:
apply unit_inv_conj_not_neg_zeta_runity_aux hζ u hp
Proof state after:
no goals