internlm/Lean-Github huggingface dataset:
Theorem: exists_int_sModEq
Proof state before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H :
  ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      pb.gen * ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred =
    x
⊢ ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      pb.gen * ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred ≡
    ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Tactic:
rw [SModEq.sub_mem, mul_one, add_sub_cancel_left, mul_comm, mem_span_singleton']
Proof state after:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H :
  ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      pb.gen * ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred =
    x
⊢ ∃ a, a * pb.gen = (∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred) * pb.gen
Theorem: exists_int_sModEq
Proof state before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H :
  ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      pb.gen * ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred =
    x
⊢ ∃ a, a * pb.gen = (∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred) * pb.gen
Tactic:
exact ⟨_, rfl⟩
Proof state after:
no goals
Theorem: exists_int_sModEq
Proof state before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
⊢ ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
Tactic:
rintro ⟨i, hi⟩
Proof state after:
case mk
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ ↑((pb.basis.repr x) ↑⟨i, hi⟩) * pb.gen ^ ↑↑⟨i, hi⟩ = ↑((pb.basis.repr x) ↑⟨i, hi⟩) * pb.gen ^ (↑↑⟨i, hi⟩).pred.succ
Theorem: exists_int_sModEq
Proof state before:
case mk
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ ↑((pb.basis.repr x) ↑⟨i, hi⟩) * pb.gen ^ ↑↑⟨i, hi⟩ = ↑((pb.basis.repr x) ↑⟨i, hi⟩) * pb.gen ^ (↑↑⟨i, hi⟩).pred.succ
Tactic:
congr 1
Proof state after:
case mk.e_a
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ pb.gen ^ ↑↑⟨i, hi⟩ = pb.gen ^ (↑↑⟨i, hi⟩).pred.succ
Theorem: exists_int_sModEq
Proof state before:
case mk.e_a
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ pb.gen ^ ↑↑⟨i, hi⟩ = pb.gen ^ (↑↑⟨i, hi⟩).pred.succ
Tactic:
rw [succ_pred_eq_of_pos]
Proof state after:
case mk.e_a
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ 0 < ↑↑⟨i, hi⟩
Theorem: exists_int_sModEq
Proof state before:
case mk.e_a
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ 0 < ↑↑⟨i, hi⟩
Tactic:
rw [Subtype.coe_mk]
Proof state after:
case mk.e_a
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ 0 < ↑i
Theorem: exists_int_sModEq
Proof state before:
case mk.e_a
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ 0 < ↑i
Tactic:
refine' Nat.pos_of_ne_zero fun h => _
Proof state after:
case mk.e_a
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
h : ↑i = 0
⊢ False
Theorem: exists_int_sModEq
Proof state before:
case mk.e_a
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
h : ↑i = 0
⊢ False
Tactic:
cases' i with i₁ hi₁
Proof state after:
case mk.e_a.mk
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i₁ : ℕ
hi₁ : i₁ < pb.dim
hi : ⟨i₁, hi₁⟩ ∈ univ.erase ⟨0, ⋯⟩
h : ↑⟨i₁, hi₁⟩ = 0
⊢ False
Theorem: exists_int_sModEq
Proof state before:
case mk.e_a.mk
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i₁ : ℕ
hi₁ : i₁ < pb.dim
hi : ⟨i₁, hi₁⟩ ∈ univ.erase ⟨0, ⋯⟩
h : ↑⟨i₁, hi₁⟩ = 0
⊢ False
Tactic:
simp only [Subtype.coe_mk] at h
Proof state after:
case mk.e_a.mk
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i₁ : ℕ
hi₁ : i₁ < pb.dim
hi : ⟨i₁, hi₁⟩ ∈ univ.erase ⟨0, ⋯⟩
h : i₁ = 0
⊢ False
Theorem: exists_int_sModEq
Proof state before:
case mk.e_a.mk
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i₁ : ℕ
hi₁ : i₁ < pb.dim
hi : ⟨i₁, hi₁⟩ ∈ univ.erase ⟨0, ⋯⟩
h : i₁ = 0
⊢ False
Tactic:
simp only [mem_univ, not_true, mem_erase, ne_eq, Fin.mk.injEq, and_true] at hi
Proof state after:
case mk.e_a.mk
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i₁ : ℕ
hi₁ : i₁ < pb.dim
h : i₁ = 0
hi : ¬i₁ = 0
⊢ False
Theorem: exists_int_sModEq
Proof state before:
case mk.e_a.mk
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i₁ : ℕ
hi₁ : i₁ < pb.dim
h : i₁ = 0
hi : ¬i₁ = 0
⊢ False
Tactic:
exact hi h
Proof state after:
no goals
Theorem: exists_int_sModEq
Proof state before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H : ∑ i ∈ insert ⟨0, ⋯⟩ (univ.erase ⟨0, ⋯⟩), (pb.basis.repr x) i • (fun i => pb.gen ^ ↑i) i = x
⊢ ⟨0, ⋯⟩ ∉ univ.erase ⟨0, ⋯⟩
Tactic:
exact not_mem_erase (⟨0, pb.dim_pos⟩ : Fin pb.dim) univ
Proof state after:
no goals
Theorem: norm_intCast
Proof state before:
K✝ : Type ?u.45394
inst✝³ : Field K✝
pb : PowerBasis ℤ (𝓞 K✝)
inst✝² : NumberField K✝
hpr : _root_.Prime ((norm ℚ) pb.gen)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℤ
⊢ (norm ℚ) ↑n = ↑n ^ finrank ℚ K
Tactic:
rw [← eq_intCast (algebraMap ℤ (𝓞 K)) n, IsScalarTower.algebraMap_apply ℤ (𝓞 ℚ) (𝓞 K)]
Proof state after:
K✝ : Type ?u.45394
inst✝³ : Field K✝
pb : PowerBasis ℤ (𝓞 K✝)
inst✝² : NumberField K✝
hpr : _root_.Prime ((norm ℚ) pb.gen)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℤ
⊢ (norm ℚ) ((algebraMap (𝓞 ℚ) (𝓞 K)) ((algebraMap ℤ (𝓞 ℚ)) n)) = ↑n ^ finrank ℚ K
Theorem: norm_intCast
Proof state before:
K✝ : Type ?u.45394
inst✝³ : Field K✝
pb : PowerBasis ℤ (𝓞 K✝)
inst✝² : NumberField K✝
hpr : _root_.Prime ((norm ℚ) pb.gen)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℤ
⊢ (norm ℚ) ((algebraMap (𝓞 ℚ) (𝓞 K)) ((algebraMap ℤ (𝓞 ℚ)) n)) = ↑n ^ finrank ℚ K
Tactic:
simp only [norm_algebraMap, algebraMap_int_eq, Int.coe_castRingHom, eq_intCast, Int.cast_pow]
Proof state after:
no goals
Theorem: zeta_sub_one_pow_dvd_poly
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
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
⊢ C ((↑hζ.unit' - 1) ^ ↑p) ∣ (C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u
Tactic:
rw [← dvd_sub_left (_root_.map_dvd C hcong), add_sub_assoc, C.map_sub (u : 𝓞 K), ← sub_add,
  sub_self, map_one, zero_add]
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
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
⊢ C ((↑hζ.unit' - 1) ^ ↑p) ∣ (C (↑hζ.unit' - 1) * X - 1) ^ ↑p + 1
Theorem: zeta_sub_one_pow_dvd_poly
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
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
⊢ C ((↑hζ.unit' - 1) ^ ↑p) ∣ (C (↑hζ.unit' - 1) * X - 1) ^ ↑p + 1
Tactic:
refine dvd_C_mul_X_sub_one_pow_add_one hpri.out (PNat.coe_injective.ne hp) _ _ dvd_rfl ?_
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
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑↑p * (↑hζ.unit' - 1)
Theorem: zeta_sub_one_pow_dvd_poly
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
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑↑p * (↑hζ.unit' - 1)
Tactic:
conv_lhs => rw [← tsub_add_cancel_of_le (Nat.Prime.one_lt hpri.out).le, pow_succ]
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
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
⊢ (↑hζ.unit' - 1) ^ (↑p - 1) * (↑hζ.unit' - 1) ∣ ↑↑p * (↑hζ.unit' - 1)
Theorem: zeta_sub_one_pow_dvd_poly
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
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
⊢ (↑hζ.unit' - 1) ^ (↑p - 1) * (↑hζ.unit' - 1) ∣ ↑↑p * (↑hζ.unit' - 1)
Tactic:
exact mul_dvd_mul_right (associated_zeta_sub_one_pow_prime hζ).dvd _
Proof state after:
no goals
Theorem: KummersLemma.natDegree_poly_aux
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
⊢ ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).natDegree = ↑p
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
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).natDegree = ↑p
Theorem: KummersLemma.natDegree_poly_aux
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).natDegree = ↑p
Tactic:
rw [natDegree_add_C, natDegree_pow, ← C.map_one, natDegree_sub_C, natDegree_mul_X, natDegree_C,
  zero_add, mul_one]
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
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ C (↑hζ.unit' - 1) ≠ 0
Theorem: KummersLemma.natDegree_poly_aux
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ C (↑hζ.unit' - 1) ≠ 0
Tactic:
exact C_ne_zero.mpr (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt)
Proof state after:
no goals
Theorem: KummersLemma.monic_poly_aux
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
⊢ ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).leadingCoeff = (↑hζ.unit' - 1) ^ ↑p
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
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).leadingCoeff = (↑hζ.unit' - 1) ^ ↑p
Theorem: KummersLemma.monic_poly_aux
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).leadingCoeff = (↑hζ.unit' - 1) ^ ↑p
Tactic:
trans leadingCoeff ((C (hζ.unit' - 1 : 𝓞 K) * X - 1) ^ (p : ℕ))
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
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).leadingCoeff = ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p).leadingCoeff

K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p).leadingCoeff = (↑hζ.unit' - 1) ^ ↑p
Theorem: KummersLemma.monic_poly_aux
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).leadingCoeff = ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p).leadingCoeff
Tactic:
rw [leadingCoeff, leadingCoeff, coeff_add]
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
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p).coeff ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).natDegree +
      (C ↑u).coeff ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).natDegree =
    ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p).coeff ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p).natDegree
Theorem: KummersLemma.monic_poly_aux
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p).coeff ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).natDegree +
      (C ↑u).coeff ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).natDegree =
    ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p).coeff ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p).natDegree
Tactic:
nth_rewrite 1 [natDegree_add_C]
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
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p).coeff ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p).natDegree +
      (C ↑u).coeff ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).natDegree =
    ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p).coeff ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p).natDegree
Theorem: KummersLemma.monic_poly_aux
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p).coeff ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p).natDegree +
      (C ↑u).coeff ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).natDegree =
    ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p).coeff ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p).natDegree
Tactic:
convert add_zero _ using 2
Proof state after:
case h.e'_2.h.e'_6
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ (C ↑u).coeff ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).natDegree = 0
Theorem: KummersLemma.monic_poly_aux
Proof state before:
case h.e'_2.h.e'_6
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ (C ↑u).coeff ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).natDegree = 0
Tactic:
rw [natDegree_poly_aux hζ, coeff_C, if_neg p.pos.ne.symm]
Proof state after:
no goals
Theorem: KummersLemma.monic_poly_aux
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p).leadingCoeff = (↑hζ.unit' - 1) ^ ↑p
Tactic:
rw [leadingCoeff_pow, ← C.map_one, leadingCoeff, natDegree_sub_C, natDegree_mul_X]
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
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ (C (↑hζ.unit' - 1) * X - C 1).coeff ((C (↑hζ.unit' - 1)).natDegree + 1) ^ ↑p = (↑hζ.unit' - 1) ^ ↑p

K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ C (↑hζ.unit' - 1) ≠ 0
Theorem: KummersLemma.monic_poly_aux
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ (C (↑hζ.unit' - 1) * X - C 1).coeff ((C (↑hζ.unit' - 1)).natDegree + 1) ^ ↑p = (↑hζ.unit' - 1) ^ ↑p

K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ C (↑hζ.unit' - 1) ≠ 0
Tactic:
simp only [map_one, natDegree_C, zero_add, coeff_sub, coeff_mul_X, coeff_C, ite_true,
  coeff_one, ite_false, sub_zero]
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
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ C (↑hζ.unit' - 1) ≠ 0
Theorem: KummersLemma.monic_poly_aux
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ C (↑hζ.unit' - 1) ≠ 0
Tactic:
exact C_ne_zero.mpr (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt)
Proof state after:
no goals
Theorem: KummersLemma.monic_poly
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
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
⊢ (poly hp hζ u hcong).Monic
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
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
this : Fact (↑p).Prime
⊢ (poly hp hζ u hcong).Monic