internlm/Lean-Github huggingface dataset:
Theorem: dvd_coeff_cycl_integer
Proof state before:
case neg.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
hf : ∃ i, f i = 0
m : ℤ
ζ' : L := ↑ζ
this : Fact (↑p).Prime
hζ' : IsPrimitiveRoot ζ' ↑p
hcoe : ζ = ⟨ζ', ⋯⟩
hlast : (Fin.castOrderIso ⋯) (Fin.last (↑p).pred) = ⟨(↑p).pred, ⋯⟩
h : ∀ (x : Fin (↑p).pred), (Fin.castOrderIso ⋯) (Fin.castSuccEmb x) = ⟨↑x, ⋯⟩
b : PowerBasis ℤ (𝓞 L) := hζ'.integralPowerBasis'
hb : b = hζ'.integralPowerBasis'
hdim : b.dim = (↑p).pred
last_dvd : m ∣ f ⟨(↑p).pred, ⋯⟩
j : Fin ↑p
H : ¬j = ⟨↑p - 1, ⋯⟩
hj : ↑j < ↑p - 1
y : 𝓞 L
hy :
  f ((Fin.castOrderIso ⋯) ((Fin.castOrderIso hdim) ((Fin.castOrderIso ⋯) ⟨↑j, hj⟩)).castSucc) - f ⟨(↑p).pred, ⋯⟩ =
    (b.basis.coord ((Fin.castOrderIso ⋯) ⟨↑j, hj⟩)) (↑m * y)
⊢ m ∣ f j
Tactic:
simp only [Fin.castOrderIso_apply, Fin.cast_mk, Fin.castSucc_mk, Fin.eta, Basis.coord_apply,
  sub_eq_iff_eq_add] at hy
Proof state after:
case neg.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
hf : ∃ i, f i = 0
m : ℤ
ζ' : L := ↑ζ
this : Fact (↑p).Prime
hζ' : IsPrimitiveRoot ζ' ↑p
hcoe : ζ = ⟨ζ', ⋯⟩
hlast : (Fin.castOrderIso ⋯) (Fin.last (↑p).pred) = ⟨(↑p).pred, ⋯⟩
h : ∀ (x : Fin (↑p).pred), (Fin.castOrderIso ⋯) (Fin.castSuccEmb x) = ⟨↑x, ⋯⟩
b : PowerBasis ℤ (𝓞 L) := hζ'.integralPowerBasis'
hb : b = hζ'.integralPowerBasis'
hdim : b.dim = (↑p).pred
last_dvd : m ∣ f ⟨(↑p).pred, ⋯⟩
j : Fin ↑p
H : ¬j = ⟨↑p - 1, ⋯⟩
hj : ↑j < ↑p - 1
y : 𝓞 L
hy : f j = (b.basis.repr (↑m * y)) ⟨↑j, ⋯⟩ + f ⟨(↑p).pred, ⋯⟩
⊢ m ∣ f j
Theorem: dvd_coeff_cycl_integer
Proof state before:
case neg.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
hf : ∃ i, f i = 0
m : ℤ
ζ' : L := ↑ζ
this : Fact (↑p).Prime
hζ' : IsPrimitiveRoot ζ' ↑p
hcoe : ζ = ⟨ζ', ⋯⟩
hlast : (Fin.castOrderIso ⋯) (Fin.last (↑p).pred) = ⟨(↑p).pred, ⋯⟩
h : ∀ (x : Fin (↑p).pred), (Fin.castOrderIso ⋯) (Fin.castSuccEmb x) = ⟨↑x, ⋯⟩
b : PowerBasis ℤ (𝓞 L) := hζ'.integralPowerBasis'
hb : b = hζ'.integralPowerBasis'
hdim : b.dim = (↑p).pred
last_dvd : m ∣ f ⟨(↑p).pred, ⋯⟩
j : Fin ↑p
H : ¬j = ⟨↑p - 1, ⋯⟩
hj : ↑j < ↑p - 1
y : 𝓞 L
hy : f j = (b.basis.repr (↑m * y)) ⟨↑j, ⋯⟩ + f ⟨(↑p).pred, ⋯⟩
⊢ m ∣ f j
Tactic:
obtain ⟨n, hn⟩ := b.basis.dvd_coord_smul ((Fin.cast hdim.symm) ⟨j, hj⟩) y m
Proof state after:
case neg.intro.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
hf : ∃ i, f i = 0
m : ℤ
ζ' : L := ↑ζ
this : Fact (↑p).Prime
hζ' : IsPrimitiveRoot ζ' ↑p
hcoe : ζ = ⟨ζ', ⋯⟩
hlast : (Fin.castOrderIso ⋯) (Fin.last (↑p).pred) = ⟨(↑p).pred, ⋯⟩
h : ∀ (x : Fin (↑p).pred), (Fin.castOrderIso ⋯) (Fin.castSuccEmb x) = ⟨↑x, ⋯⟩
b : PowerBasis ℤ (𝓞 L) := hζ'.integralPowerBasis'
hb : b = hζ'.integralPowerBasis'
hdim : b.dim = (↑p).pred
last_dvd : m ∣ f ⟨(↑p).pred, ⋯⟩
j : Fin ↑p
H : ¬j = ⟨↑p - 1, ⋯⟩
hj : ↑j < ↑p - 1
y : 𝓞 L
hy : f j = (b.basis.repr (↑m * y)) ⟨↑j, ⋯⟩ + f ⟨(↑p).pred, ⋯⟩
n : ℤ
hn : (b.basis.coord (Fin.cast ⋯ ⟨↑j, hj⟩)) (m • y) = m * n
⊢ m ∣ f j
Theorem: dvd_coeff_cycl_integer
Proof state before:
case neg.intro.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
hf : ∃ i, f i = 0
m : ℤ
ζ' : L := ↑ζ
this : Fact (↑p).Prime
hζ' : IsPrimitiveRoot ζ' ↑p
hcoe : ζ = ⟨ζ', ⋯⟩
hlast : (Fin.castOrderIso ⋯) (Fin.last (↑p).pred) = ⟨(↑p).pred, ⋯⟩
h : ∀ (x : Fin (↑p).pred), (Fin.castOrderIso ⋯) (Fin.castSuccEmb x) = ⟨↑x, ⋯⟩
b : PowerBasis ℤ (𝓞 L) := hζ'.integralPowerBasis'
hb : b = hζ'.integralPowerBasis'
hdim : b.dim = (↑p).pred
last_dvd : m ∣ f ⟨(↑p).pred, ⋯⟩
j : Fin ↑p
H : ¬j = ⟨↑p - 1, ⋯⟩
hj : ↑j < ↑p - 1
y : 𝓞 L
hy : f j = (b.basis.repr (↑m * y)) ⟨↑j, ⋯⟩ + f ⟨(↑p).pred, ⋯⟩
n : ℤ
hn : (b.basis.coord (Fin.cast ⋯ ⟨↑j, hj⟩)) (m • y) = m * n
⊢ m ∣ f j
Tactic:
rw [hy, ← smul_eq_mul, ← zsmul_eq_smul_cast, ← b.basis.coord_apply, ← Fin.cast_mk, hn]
Proof state after:
case neg.intro.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
hf : ∃ i, f i = 0
m : ℤ
ζ' : L := ↑ζ
this : Fact (↑p).Prime
hζ' : IsPrimitiveRoot ζ' ↑p
hcoe : ζ = ⟨ζ', ⋯⟩
hlast : (Fin.castOrderIso ⋯) (Fin.last (↑p).pred) = ⟨(↑p).pred, ⋯⟩
h : ∀ (x : Fin (↑p).pred), (Fin.castOrderIso ⋯) (Fin.castSuccEmb x) = ⟨↑x, ⋯⟩
b : PowerBasis ℤ (𝓞 L) := hζ'.integralPowerBasis'
hb : b = hζ'.integralPowerBasis'
hdim : b.dim = (↑p).pred
last_dvd : m ∣ f ⟨(↑p).pred, ⋯⟩
j : Fin ↑p
H : ¬j = ⟨↑p - 1, ⋯⟩
hj : ↑j < ↑p - 1
y : 𝓞 L
hy : f j = (b.basis.repr (↑m * y)) ⟨↑j, ⋯⟩ + f ⟨(↑p).pred, ⋯⟩
n : ℤ
hn : (b.basis.coord (Fin.cast ⋯ ⟨↑j, hj⟩)) (m • y) = m * n
⊢ m ∣ m * n + f ⟨(↑p).pred, ⋯⟩
Theorem: dvd_coeff_cycl_integer
Proof state before:
case neg.intro.intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
hf : ∃ i, f i = 0
m : ℤ
ζ' : L := ↑ζ
this : Fact (↑p).Prime
hζ' : IsPrimitiveRoot ζ' ↑p
hcoe : ζ = ⟨ζ', ⋯⟩
hlast : (Fin.castOrderIso ⋯) (Fin.last (↑p).pred) = ⟨(↑p).pred, ⋯⟩
h : ∀ (x : Fin (↑p).pred), (Fin.castOrderIso ⋯) (Fin.castSuccEmb x) = ⟨↑x, ⋯⟩
b : PowerBasis ℤ (𝓞 L) := hζ'.integralPowerBasis'
hb : b = hζ'.integralPowerBasis'
hdim : b.dim = (↑p).pred
last_dvd : m ∣ f ⟨(↑p).pred, ⋯⟩
j : Fin ↑p
H : ¬j = ⟨↑p - 1, ⋯⟩
hj : ↑j < ↑p - 1
y : 𝓞 L
hy : f j = (b.basis.repr (↑m * y)) ⟨↑j, ⋯⟩ + f ⟨(↑p).pred, ⋯⟩
n : ℤ
hn : (b.basis.coord (Fin.cast ⋯ ⟨↑j, hj⟩)) (m • y) = m * n
⊢ m ∣ m * n + f ⟨(↑p).pred, ⋯⟩
Tactic:
exact dvd_add (dvd_mul_right _ _) last_dvd
Proof state after:
no goals
Theorem: dvd_coeff_cycl_integer
Proof state before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
hf : ∃ i, f i = 0
m : ℤ
hdiv : ↑m ∣ ∑ j : Fin ↑p, f j • ζ ^ ↑j
ζ' : L := ↑ζ
this : Fact (↑p).Prime
hζ' : IsPrimitiveRoot ζ' ↑p
⊢ ζ = ⟨ζ', ⋯⟩
Tactic:
rfl
Proof state after:
no goals
Theorem: dvd_coeff_cycl_integer
Proof state before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
hf : ∃ i, f i = 0
m : ℤ
hdiv : ↑m ∣ ∑ j : Fin ↑p, f j • ζ ^ ↑j
ζ' : L := ↑ζ
this : Fact (↑p).Prime
hζ' : IsPrimitiveRoot ζ' ↑p
hcoe : ζ = ⟨ζ', ⋯⟩
hlast : (Fin.castOrderIso ⋯) (Fin.last (↑p).pred) = ⟨(↑p).pred, ⋯⟩
h : ∀ (x : Fin (↑p).pred), (Fin.castOrderIso ⋯) (Fin.castSuccEmb x) = ⟨↑x, ⋯⟩
b : PowerBasis ℤ (𝓞 L) := hζ'.integralPowerBasis'
hb : b = hζ'.integralPowerBasis'
⊢ b.dim = (↑p).pred
Tactic:
rw [hζ'.power_basis_int'_dim, totient_prime hp,
pred_eq_sub_one]
Proof state after:
no goals
Theorem: dvd_coeff_cycl_integer
Proof state before:
case pos
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
hf : ∃ i, f i = 0
m : ℤ
hdiv : ↑m ∣ ∑ j : Fin ↑p, f j • ζ ^ ↑j
ζ' : L := ↑ζ
this : Fact (↑p).Prime
hζ' : IsPrimitiveRoot ζ' ↑p
hcoe : ζ = ⟨ζ', ⋯⟩
hlast : (Fin.castOrderIso ⋯) (Fin.last (↑p).pred) = ⟨(↑p).pred, ⋯⟩
h : ∀ (x : Fin (↑p).pred), (Fin.castOrderIso ⋯) (Fin.castSuccEmb x) = ⟨↑x, ⋯⟩
b : PowerBasis ℤ (𝓞 L) := hζ'.integralPowerBasis'
hb : b = hζ'.integralPowerBasis'
hdim : b.dim = (↑p).pred
last_dvd : m ∣ f ⟨(↑p).pred, ⋯⟩
j : Fin ↑p
H : j = ⟨↑p - 1, ⋯⟩
⊢ m ∣ f j
Tactic:
simpa [H] using last_dvd
Proof state after:
no goals
Theorem: dvd_coeff_cycl_integer
Proof state before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
hf : ∃ i, f i = 0
m : ℤ
hdiv : ↑m ∣ ∑ j : Fin ↑p, f j • ζ ^ ↑j
ζ' : L := ↑ζ
this : Fact (↑p).Prime
hζ' : IsPrimitiveRoot ζ' ↑p
hcoe : ζ = ⟨ζ', ⋯⟩
hlast : (Fin.castOrderIso ⋯) (Fin.last (↑p).pred) = ⟨(↑p).pred, ⋯⟩
h : ∀ (x : Fin (↑p).pred), (Fin.castOrderIso ⋯) (Fin.castSuccEmb x) = ⟨↑x, ⋯⟩
b : PowerBasis ℤ (𝓞 L) := hζ'.integralPowerBasis'
hb : b = hζ'.integralPowerBasis'
hdim : b.dim = (↑p).pred
last_dvd : m ∣ f ⟨(↑p).pred, ⋯⟩
j : Fin ↑p
H : ¬j = ⟨↑p - 1, ⋯⟩
⊢ ↑j < ↑p - 1
Tactic:
by_contra! habs
Proof state after:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
hf : ∃ i, f i = 0
m : ℤ
hdiv : ↑m ∣ ∑ j : Fin ↑p, f j • ζ ^ ↑j
ζ' : L := ↑ζ
this : Fact (↑p).Prime
hζ' : IsPrimitiveRoot ζ' ↑p
hcoe : ζ = ⟨ζ', ⋯⟩
hlast : (Fin.castOrderIso ⋯) (Fin.last (↑p).pred) = ⟨(↑p).pred, ⋯⟩
h : ∀ (x : Fin (↑p).pred), (Fin.castOrderIso ⋯) (Fin.castSuccEmb x) = ⟨↑x, ⋯⟩
b : PowerBasis ℤ (𝓞 L) := hζ'.integralPowerBasis'
hb : b = hζ'.integralPowerBasis'
hdim : b.dim = (↑p).pred
last_dvd : m ∣ f ⟨(↑p).pred, ⋯⟩
j : Fin ↑p
H : ¬j = ⟨↑p - 1, ⋯⟩
habs : ↑p - 1 ≤ ↑j
⊢ False
Theorem: dvd_coeff_cycl_integer
Proof state before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
hf : ∃ i, f i = 0
m : ℤ
hdiv : ↑m ∣ ∑ j : Fin ↑p, f j • ζ ^ ↑j
ζ' : L := ↑ζ
this : Fact (↑p).Prime
hζ' : IsPrimitiveRoot ζ' ↑p
hcoe : ζ = ⟨ζ', ⋯⟩
hlast : (Fin.castOrderIso ⋯) (Fin.last (↑p).pred) = ⟨(↑p).pred, ⋯⟩
h : ∀ (x : Fin (↑p).pred), (Fin.castOrderIso ⋯) (Fin.castSuccEmb x) = ⟨↑x, ⋯⟩
b : PowerBasis ℤ (𝓞 L) := hζ'.integralPowerBasis'
hb : b = hζ'.integralPowerBasis'
hdim : b.dim = (↑p).pred
last_dvd : m ∣ f ⟨(↑p).pred, ⋯⟩
j : Fin ↑p
H : ¬j = ⟨↑p - 1, ⋯⟩
habs : ↑p - 1 ≤ ↑j
⊢ False
Tactic:
simp [le_antisymm habs (le_pred_of_lt (Fin.is_lt j))] at H
Proof state after:
no goals
Theorem: PowerBasis.rat_hom_ext
Proof state before:
S : Type u_1
S' : Type u_2
inst✝¹ : CommRing S
hS : Algebra ℚ S
inst✝ : Ring S'
hS' : Algebra ℚ S'
pb : PowerBasis ℚ S
f g : S →+* S'
h : f pb.gen = g pb.gen
f' : S →ₐ[ℚ] S' := f.toRatAlgHom
g' : S →ₐ[ℚ] S' := g.toRatAlgHom
⊢ ∀ (x : S), f x = g x
Tactic:
convert DFunLike.ext_iff.mp (pb.algHom_ext (show f' pb.gen = g' pb.gen from h))
Proof state after:
no goals
Theorem: galConj_zeta
Proof state before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ (galConj K p) (zeta p ℚ K) = (zeta p ℚ K)⁻¹
Tactic:
let hζ := zeta_spec p ℚ K
Proof state after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑p
hζ : IsPrimitiveRoot (zeta p ℚ K) ↑p := zeta_spec p ℚ K
⊢ (galConj K p) (zeta p ℚ K) = (zeta p ℚ K)⁻¹
Theorem: galConj_zeta
Proof state before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑p
hζ : IsPrimitiveRoot (zeta p ℚ K) ↑p := zeta_spec p ℚ K
⊢ (galConj K p) (zeta p ℚ K) = (zeta p ℚ K)⁻¹
Tactic:
simp only [galConj, Units.coe_neg_one, autEquivPow_symm_apply, AlgEquiv.coe_algHom,
  PowerBasis.equivOfMinpoly_apply]
Proof state after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑p
hζ : IsPrimitiveRoot (zeta p ℚ K) ↑p := zeta_spec p ℚ K
⊢ ((IsPrimitiveRoot.powerBasis ℚ ⋯).lift (IsPrimitiveRoot.powerBasis ℚ ⋯).gen ⋯) (zeta p ℚ K) = (zeta p ℚ K)⁻¹
Theorem: galConj_zeta
Proof state before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑p
hζ : IsPrimitiveRoot (zeta p ℚ K) ↑p := zeta_spec p ℚ K
⊢ ((IsPrimitiveRoot.powerBasis ℚ ⋯).lift (IsPrimitiveRoot.powerBasis ℚ ⋯).gen ⋯) (zeta p ℚ K) = (zeta p ℚ K)⁻¹
Tactic:
convert (hζ.powerBasis ℚ).lift_gen (S' := K) _ _
Proof state after:
case h.e'_3
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑p
hζ : IsPrimitiveRoot (zeta p ℚ K) ↑p := zeta_spec p ℚ K
⊢ (zeta p ℚ K)⁻¹ = (IsPrimitiveRoot.powerBasis ℚ ⋯).gen
Theorem: galConj_zeta
Proof state before:
case h.e'_3
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑p
hζ : IsPrimitiveRoot (zeta p ℚ K) ↑p := zeta_spec p ℚ K
⊢ (zeta p ℚ K)⁻¹ = (IsPrimitiveRoot.powerBasis ℚ ⋯).gen
Tactic:
rw [IsPrimitiveRoot.powerBasis_gen, ZMod.val_neg_one' p.pos,
  pow_sub₀ _ (hζ.ne_zero p.ne_zero) p.pos, pow_one, hζ.pow_eq_one, one_mul]
Proof state after:
no goals
Theorem: galConj_zeta_runity
Proof state before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ (galConj K p) ζ = ζ⁻¹
Tactic:
obtain ⟨t, _, rfl⟩ := (zeta_spec p ℚ K).eq_pow_of_pow_eq_one hζ.pow_eq_one p.pos
Proof state after:
case intro.intro
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
t : ℕ
left✝ : t < ↑p
hζ : IsPrimitiveRoot (zeta p ℚ K ^ t) ↑p
⊢ (galConj K p) (zeta p ℚ K ^ t) = (zeta p ℚ K ^ t)⁻¹
Theorem: galConj_zeta_runity
Proof state before:
case intro.intro
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
t : ℕ
left✝ : t < ↑p
hζ : IsPrimitiveRoot (zeta p ℚ K ^ t) ↑p
⊢ (galConj K p) (zeta p ℚ K ^ t) = (zeta p ℚ K ^ t)⁻¹
Tactic:
rw [map_pow, galConj_zeta, inv_pow]
Proof state after:
no goals
Theorem: galConj_zeta_runity_pow
Proof state before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
⊢ (galConj K p) (ζ ^ n) = ζ⁻¹ ^ n
Tactic:
rw [map_pow, galConj_zeta_runity hζ]
Proof state after:
no goals
Theorem: conj_norm_one
Proof state before:
K : Type ?u.24099
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x : ℂ
h : Complex.abs x = 1
⊢ (starRingEnd ℂ) x = x⁻¹
Tactic:
rw [← Complex.abs_mul_exp_arg_mul_I x, h, Complex.ofReal_one, one_mul, ← Complex.exp_conj, ←
  Complex.exp_neg, map_mul, Complex.conj_I, mul_neg, Complex.conj_ofReal]
Proof state after:
no goals
Theorem: embedding_conj
Proof state before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x : K
φ : K →+* ℂ
⊢ (starRingEnd ℂ) (φ x) = φ ((galConj K p) x)
Tactic:
change RingHom.comp conj φ x = (φ.comp <| ↑(galConj K p)) x
Proof state after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x : K
φ : K →+* ℂ
⊢ ((starRingEnd ℂ).comp φ) x = (φ.comp ↑(galConj K p)) x
Theorem: embedding_conj
Proof state before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x : K
φ : K →+* ℂ
⊢ ((starRingEnd ℂ).comp φ) x = (φ.comp ↑(galConj K p)) x
Tactic:
revert x
Proof state after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
⊢ ∀ (x : K), ((starRingEnd ℂ).comp φ) x = (φ.comp ↑(galConj K p)) x
Theorem: embedding_conj
Proof state before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
⊢ ∀ (x : K), ((starRingEnd ℂ).comp φ) x = (φ.comp ↑(galConj K p)) x
Tactic:
suffices φ (galConj K p ζ) = conj (φ ζ)
  by
  rw [← Function.funext_iff]
  congr
  rw [DFunLike.coe_fn_eq]
  apply (hζ.powerBasis ℚ).rat_hom_ext
  exact this.symm
Proof state after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
⊢ φ ((galConj K p) ζ) = (starRingEnd ℂ) (φ ζ)
Theorem: embedding_conj
Proof state before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
⊢ φ ((galConj K p) ζ) = (starRingEnd ℂ) (φ ζ)
Tactic:
rw [conj_norm_one, galConj_zeta_runity hζ, map_inv₀]
Proof state after:
case h
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
⊢ Complex.abs (φ ζ) = 1
Theorem: embedding_conj
Proof state before:
case h
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
⊢ Complex.abs (φ ζ) = 1
Tactic:
refine' Complex.norm_eq_one_of_pow_eq_one _ p.ne_zero
Proof state after:
case h
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
⊢ φ ζ ^ ↑p = 1
Theorem: embedding_conj
Proof state before:
case h
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
⊢ φ ζ ^ ↑p = 1
Tactic:
rw [← map_pow, hζ.pow_eq_one, map_one]
Proof state after:
no goals
Theorem: embedding_conj
Proof state before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
this : φ ((galConj K p) ζ) = (starRingEnd ℂ) (φ ζ)
⊢ ∀ (x : K), ((starRingEnd ℂ).comp φ) x = (φ.comp ↑(galConj K p)) x
Tactic:
rw [← Function.funext_iff]
Proof state after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
this : φ ((galConj K p) ζ) = (starRingEnd ℂ) (φ ζ)
⊢ (fun x => ((starRingEnd ℂ).comp φ) x) = fun x => (φ.comp ↑(galConj K p)) x
Theorem: embedding_conj
Proof state before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
this : φ ((galConj K p) ζ) = (starRingEnd ℂ) (φ ζ)
⊢ (fun x => ((starRingEnd ℂ).comp φ) x) = fun x => (φ.comp ↑(galConj K p)) x
Tactic:
rw [DFunLike.coe_fn_eq]
Proof state after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
this : φ ((galConj K p) ζ) = (starRingEnd ℂ) (φ ζ)
⊢ (starRingEnd ℂ).comp φ = φ.comp ↑(galConj K p)
Theorem: embedding_conj
Proof state before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
this : φ ((galConj K p) ζ) = (starRingEnd ℂ) (φ ζ)
⊢ (starRingEnd ℂ).comp φ = φ.comp ↑(galConj K p)
Tactic:
apply (hζ.powerBasis ℚ).rat_hom_ext
Proof state after:
case h
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
this : φ ((galConj K p) ζ) = (starRingEnd ℂ) (φ ζ)
⊢ ((starRingEnd ℂ).comp φ) (IsPrimitiveRoot.powerBasis ℚ hζ).gen =
    (φ.comp ↑(galConj K p)) (IsPrimitiveRoot.powerBasis ℚ hζ).gen
Theorem: embedding_conj
Proof state before:
case h
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
this : φ ((galConj K p) ζ) = (starRingEnd ℂ) (φ ζ)
⊢ ((starRingEnd ℂ).comp φ) (IsPrimitiveRoot.powerBasis ℚ hζ).gen =
    (φ.comp ↑(galConj K p)) (IsPrimitiveRoot.powerBasis ℚ hζ).gen
Tactic:
exact this.symm
Proof state after:
no goals
Theorem: galConj_idempotent
Proof state before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ (galConj K p).trans (galConj K p) = AlgEquiv.refl
Tactic:
rw [← AlgEquiv.aut_mul, galConj, ← map_mul, neg_one_mul, neg_neg, map_one]
Proof state after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ 1 = AlgEquiv.refl
Theorem: galConj_idempotent
Proof state before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ 1 = AlgEquiv.refl
Tactic:
rfl
Proof state after:
no goals
Theorem: unit_lemma_val_one
Proof state before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
φ : K →+* ℂ
⊢ Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u * (algebraMap (𝓞 K) K) ↑((unitGalConj K p) u)⁻¹)) = 1
Tactic:
rw [map_mul, IsAbsoluteValue.abv_mul Complex.abs, ← zpow_neg_one, NumberField.Units.coe_zpow,
  zpow_neg_one, map_inv₀, ← unitGalConj_spec,
  ← embedding_conj <| zeta_spec p ℚ K]
Proof state after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
φ : K →+* ℂ
⊢ Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u)) * Complex.abs ((starRingEnd ℂ) (φ ((algebraMap (𝓞 K) K) ↑u)))⁻¹ = 1
Theorem: unit_lemma_val_one
Proof state before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
φ : K →+* ℂ
⊢ Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u)) * Complex.abs ((starRingEnd ℂ) (φ ((algebraMap (𝓞 K) K) ↑u)))⁻¹ = 1
Tactic:
simp only [map_inv₀, Complex.abs_conj]
Proof state after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
φ : K →+* ℂ
⊢ Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u)) * (Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u)))⁻¹ = 1
Theorem: unit_lemma_val_one
Proof state before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
φ : K →+* ℂ
⊢ Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u)) * (Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u)))⁻¹ = 1
Tactic:
rw [mul_inv_eq_one₀]
Proof state after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
φ : K →+* ℂ
⊢ Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u)) ≠ 0
Theorem: unit_lemma_val_one
Proof state before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
φ : K →+* ℂ
⊢ Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u)) ≠ 0
Tactic:
intro h
Proof state after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
φ : K →+* ℂ
h : Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u)) = 0
⊢ False
Theorem: unit_lemma_val_one
Proof state before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
φ : K →+* ℂ
h : Complex.abs (φ ((algebraMap (𝓞 K) K) ↑u)) = 0
⊢ False
Tactic:
simp at h
Proof state after:
no goals
Theorem: zeta_sub_one_dvd
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) }
⊢ π ∣ x ^ ↑p + y ^ ↑p
Tactic:
rw [e, mul_pow, ← pow_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) }
⊢ π ∣ ↑ε * (π ^ ((m + 1) * ↑p) * z ^ ↑p)