internlm/Lean-Github huggingface dataset:
Theorem: KummersLemma.map_poly
Proof state before:
case h.e'_2
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
i : ℕ
this :
  ↑(((C ↑hζ.unit' - 1) ^ ↑p * poly hp hζ u hcong).coeff i) =
    (((C ζ - 1) * X - 1) ^ ↑p).coeff i + (C ((algebraMap (𝓞 K) K) ↑u)).coeff i
⊢ (ζ - 1) ^ ↑p * (map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i =
    (map (algebraMap (𝓞 K) K) ((C ↑hζ.unit' - 1) ^ ↑p * poly hp hζ u hcong)).coeff i
Tactic:
simp only [coeff_map, Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_sub, map_C,
  IsPrimitiveRoot.coe_unit'_coe, Polynomial.map_one]
Proof state after:
case h.e'_2
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
i : ℕ
this :
  ↑(((C ↑hζ.unit' - 1) ^ ↑p * poly hp hζ u hcong).coeff i) =
    (((C ζ - 1) * X - 1) ^ ↑p).coeff i + (C ((algebraMap (𝓞 K) K) ↑u)).coeff i
⊢ (ζ - 1) ^ ↑p * (algebraMap (𝓞 K) K) ((poly hp hζ u hcong).coeff i) =
    ((C ζ - 1) ^ ↑p * map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i
Theorem: KummersLemma.map_poly
Proof state before:
case h.e'_2
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
i : ℕ
this :
  ↑(((C ↑hζ.unit' - 1) ^ ↑p * poly hp hζ u hcong).coeff i) =
    (((C ζ - 1) * X - 1) ^ ↑p).coeff i + (C ((algebraMap (𝓞 K) K) ↑u)).coeff i
⊢ (ζ - 1) ^ ↑p * (algebraMap (𝓞 K) K) ((poly hp hζ u hcong).coeff i) =
    ((C ζ - 1) ^ ↑p * map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i
Tactic:
rw [← Polynomial.coeff_map, mul_comm, ← Polynomial.coeff_mul_C, mul_comm]
Proof state after:
case h.e'_2
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
i : ℕ
this :
  ↑(((C ↑hζ.unit' - 1) ^ ↑p * poly hp hζ u hcong).coeff i) =
    (((C ζ - 1) * X - 1) ^ ↑p).coeff i + (C ((algebraMap (𝓞 K) K) ↑u)).coeff i
⊢ (C ((ζ - 1) ^ ↑p) * map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i =
    ((C ζ - 1) ^ ↑p * map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i
Theorem: KummersLemma.map_poly
Proof state before:
case h.e'_2
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
i : ℕ
this :
  ↑(((C ↑hζ.unit' - 1) ^ ↑p * poly hp hζ u hcong).coeff i) =
    (((C ζ - 1) * X - 1) ^ ↑p).coeff i + (C ((algebraMap (𝓞 K) K) ↑u)).coeff i
⊢ (C ((ζ - 1) ^ ↑p) * map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i =
    ((C ζ - 1) ^ ↑p * map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i
Tactic:
simp
Proof state after:
no goals
Theorem: KummersLemma.map_poly
Proof state before:
case a.a
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
i : ℕ
this :
  (ζ - 1) ^ ↑p * ↑((poly hp hζ u hcong).coeff i) =
    (((C ((algebraMap (𝓞 K) K) ↑hζ.unit') - 1) * X - 1) ^ ↑p).coeff i + (C ((algebraMap (𝓞 K) K) ↑u)).coeff i
⊢ ζ - 1 ≠ 0
Tactic:
exact hζ.sub_one_ne_zero hpri.out.one_lt
Proof state after:
no goals
Theorem: KummersLemma.map_poly
Proof state before:
case a.a.ha
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
i : ℕ
this :
  (ζ - 1) ^ ↑p * ↑((poly hp hζ u hcong).coeff i) =
    (((C ((algebraMap (𝓞 K) K) ↑hζ.unit') - 1) * X - 1) ^ ↑p).coeff i + (C ((algebraMap (𝓞 K) K) ↑u)).coeff i
⊢ (ζ - 1) ^ ↑p ≠ 0
Tactic:
exact pow_ne_zero _ (hζ.sub_one_ne_zero hpri.out.one_lt)
Proof state after:
no goals
Theorem: KummersLemma.irreducible_map_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
⊢ Irreducible (map (algebraMap (𝓞 K) K) (poly hp hζ u hcong))
Tactic:
rw [map_poly, ← irreducible_taylor_iff (r := 1 / (ζ - 1))]
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
⊢ Irreducible ((taylor (1 / (ζ - 1))) ((X - C (1 / (ζ - 1))) ^ ↑p + C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)))
Theorem: KummersLemma.irreducible_map_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
⊢ Irreducible ((taylor (1 / (ζ - 1))) ((X - C (1 / (ζ - 1))) ^ ↑p + C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)))
Tactic:
simp only [taylor, one_div, map_add, LinearMap.coe_mk, AddHom.coe_mk, pow_comp, sub_comp,
  X_comp, C_comp, add_sub_cancel_right]
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
⊢ Irreducible (X ^ ↑p + C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p))
Theorem: KummersLemma.irreducible_map_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
⊢ Irreducible (X ^ ↑p + C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p))
Tactic:
rw [← sub_neg_eq_add, ← (C : K →+* _).map_neg]
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
⊢ Irreducible (X ^ ↑p - C (-((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)))
Theorem: KummersLemma.irreducible_map_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
⊢ Irreducible (X ^ ↑p - C (-((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)))
Tactic:
apply X_pow_sub_C_irreducible_of_prime hpri.out
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
⊢ ∀ (b : K), b ^ ↑p ≠ -((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)
Theorem: KummersLemma.irreducible_map_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
⊢ ∀ (b : K), b ^ ↑p ≠ -((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)
Tactic:
intro b hb
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
b : K
hb : b ^ ↑p = -((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)
⊢ False
Theorem: KummersLemma.irreducible_map_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
b : K
hb : b ^ ↑p = -((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)
⊢ False
Tactic:
apply hu (- b * (ζ - 1))
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
b : K
hb : b ^ ↑p = -((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)
⊢ (-b * (ζ - 1)) ^ ↑p = (algebraMap (𝓞 K) K) ↑u
Theorem: KummersLemma.irreducible_map_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
b : K
hb : b ^ ↑p = -((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)
⊢ (-b * (ζ - 1)) ^ ↑p = (algebraMap (𝓞 K) K) ↑u
Tactic:
rw [mul_pow, (hpri.out.odd_of_ne_two (PNat.coe_injective.ne hp)).neg_pow, hb, neg_neg,
  div_mul_cancel₀ _ (pow_ne_zero _ (hζ.sub_one_ne_zero hpri.out.one_lt))]
Proof state after:
no goals
Theorem: KummersLemma.aeval_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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
m : ℕ
⊢ (aeval ((1 - ζ ^ m • α) / (algebraMap K L) (ζ - 1))) (poly hp hζ u hcong) = 0
Tactic:
have hζ' : algebraMap K L ζ - 1 ≠ 0 := by
  simpa using (algebraMap K L).injective.ne (hζ.sub_one_ne_zero hpri.out.one_lt)
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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
m : ℕ
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ (aeval ((1 - ζ ^ m • α) / (algebraMap K L) (ζ - 1))) (poly hp hζ u hcong) = 0
Theorem: KummersLemma.aeval_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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
m : ℕ
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ (aeval ((1 - ζ ^ m • α) / (algebraMap K L) (ζ - 1))) (poly hp hζ u hcong) = 0
Tactic:
rw [map_sub, map_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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
m : ℕ
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ (aeval ((1 - ζ ^ m • α) / ((algebraMap K L) ζ - 1))) (poly hp hζ u hcong) = 0
Theorem: KummersLemma.aeval_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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
m : ℕ
hζ' : (algebraMap K L) ζ - 1 ≠ 0
⊢ (aeval ((1 - ζ ^ m • α) / ((algebraMap K L) ζ - 1))) (poly hp hζ u hcong) = 0
Tactic:
have := congr_arg (aeval ((1 - ζ ^ m • α) / (algebraMap K L (ζ - 1))))
  (poly_spec hp hζ u hcong)
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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
m : ℕ
hζ' : (algebraMap K L) ζ - 1 ≠ 0
this :
  (aeval ((1 - ζ ^ m • α) / (algebraMap K L) (ζ - 1))) (C ((↑hζ.unit' - 1) ^ ↑p) * poly hp hζ u hcong) =
    (aeval ((1 - ζ ^ m • α) / (algebraMap K L) (ζ - 1))) ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u)
⊢ (aeval ((1 - ζ ^ m • α) / ((algebraMap K L) ζ - 1))) (poly hp hζ u hcong) = 0
Theorem: KummersLemma.aeval_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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
m : ℕ
hζ' : (algebraMap K L) ζ - 1 ≠ 0
this :
  (aeval ((1 - ζ ^ m • α) / (algebraMap K L) (ζ - 1))) (C ((↑hζ.unit' - 1) ^ ↑p) * poly hp hζ u hcong) =
    (aeval ((1 - ζ ^ m • α) / (algebraMap K L) (ζ - 1))) ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u)
⊢ (aeval ((1 - ζ ^ m • α) / ((algebraMap K L) ζ - 1))) (poly hp hζ u hcong) = 0
Tactic:
have hcoe : (algebraMap (𝓞 K) L) (↑hζ.unit') = algebraMap K L ζ := 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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
m : ℕ
hζ' : (algebraMap K L) ζ - 1 ≠ 0
this :
  (aeval ((1 - ζ ^ m • α) / (algebraMap K L) (ζ - 1))) (C ((↑hζ.unit' - 1) ^ ↑p) * poly hp hζ u hcong) =
    (aeval ((1 - ζ ^ m • α) / (algebraMap K L) (ζ - 1))) ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u)
hcoe : (algebraMap (𝓞 K) L) ↑hζ.unit' = (algebraMap K L) ζ
⊢ (aeval ((1 - ζ ^ m • α) / ((algebraMap K L) ζ - 1))) (poly hp hζ u hcong) = 0
Theorem: KummersLemma.aeval_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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
m : ℕ
hζ' : (algebraMap K L) ζ - 1 ≠ 0
this :
  (aeval ((1 - ζ ^ m • α) / (algebraMap K L) (ζ - 1))) (C ((↑hζ.unit' - 1) ^ ↑p) * poly hp hζ u hcong) =
    (aeval ((1 - ζ ^ m • α) / (algebraMap K L) (ζ - 1))) ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u)
hcoe : (algebraMap (𝓞 K) L) ↑hζ.unit' = (algebraMap K L) ζ
⊢ (aeval ((1 - ζ ^ m • α) / ((algebraMap K L) ζ - 1))) (poly hp hζ u hcong) = 0
Tactic:
have hcoe1 : (algebraMap (𝓞 K) L) ↑u = algebraMap K L ↑↑u := 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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
m : ℕ
hζ' : (algebraMap K L) ζ - 1 ≠ 0
this :
  (aeval ((1 - ζ ^ m • α) / (algebraMap K L) (ζ - 1))) (C ((↑hζ.unit' - 1) ^ ↑p) * poly hp hζ u hcong) =
    (aeval ((1 - ζ ^ m • α) / (algebraMap K L) (ζ - 1))) ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u)
hcoe : (algebraMap (𝓞 K) L) ↑hζ.unit' = (algebraMap K L) ζ
hcoe1 : (algebraMap (𝓞 K) L) ↑u = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
⊢ (aeval ((1 - ζ ^ m • α) / ((algebraMap K L) ζ - 1))) (poly hp hζ u hcong) = 0
Theorem: KummersLemma.aeval_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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
m : ℕ
hζ' : (algebraMap K L) ζ - 1 ≠ 0
this :
  (aeval ((1 - ζ ^ m • α) / (algebraMap K L) (ζ - 1))) (C ((↑hζ.unit' - 1) ^ ↑p) * poly hp hζ u hcong) =
    (aeval ((1 - ζ ^ m • α) / (algebraMap K L) (ζ - 1))) ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u)
hcoe : (algebraMap (𝓞 K) L) ↑hζ.unit' = (algebraMap K L) ζ
hcoe1 : (algebraMap (𝓞 K) L) ↑u = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
⊢ (aeval ((1 - ζ ^ m • α) / ((algebraMap K L) ζ - 1))) (poly hp hζ u hcong) = 0
Tactic:
simp only [map_sub, map_one, map_pow, map_mul, aeval_C, Subalgebra.algebraMap_eq, smul_pow,
  hcoe, RingHom.coe_comp, RingHom.coe_coe, Subalgebra.coe_val, Function.comp_apply, e, hcoe1,
  IsPrimitiveRoot.val_unit'_coe, map_add, aeval_X, ← mul_div_assoc, mul_div_cancel_left₀ _ hζ',
  sub_sub_cancel_left, (hpri.out.odd_of_ne_two (PNat.coe_injective.ne hp)).neg_pow] at this
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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
m : ℕ
hζ' : (algebraMap K L) ζ - 1 ≠ 0
hcoe : (algebraMap (𝓞 K) L) ↑hζ.unit' = (algebraMap K L) ζ
hcoe1 : (algebraMap (𝓞 K) L) ↑u = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
this :
  ((algebraMap K L) ζ - 1) ^ ↑p * (aeval ((1 - ζ ^ m • α) / ((algebraMap K L) ζ - 1))) (poly hp hζ u hcong) =
    -((ζ ^ m) ^ ↑p • (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)) + (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
⊢ (aeval ((1 - ζ ^ m • α) / ((algebraMap K L) ζ - 1))) (poly hp hζ u hcong) = 0
Theorem: KummersLemma.aeval_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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
m : ℕ
hζ' : (algebraMap K L) ζ - 1 ≠ 0
hcoe : (algebraMap (𝓞 K) L) ↑hζ.unit' = (algebraMap K L) ζ
hcoe1 : (algebraMap (𝓞 K) L) ↑u = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
this :
  ((algebraMap K L) ζ - 1) ^ ↑p * (aeval ((1 - ζ ^ m • α) / ((algebraMap K L) ζ - 1))) (poly hp hζ u hcong) =
    -((ζ ^ m) ^ ↑p • (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)) + (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
⊢ (aeval ((1 - ζ ^ m • α) / ((algebraMap K L) ζ - 1))) (poly hp hζ u hcong) = 0
Tactic:
rw [← pow_mul, mul_comm m, pow_mul, hζ.pow_eq_one, one_pow, one_smul, add_left_neg,
  mul_eq_zero] at this
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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
m : ℕ
hζ' : (algebraMap K L) ζ - 1 ≠ 0
hcoe : (algebraMap (𝓞 K) L) ↑hζ.unit' = (algebraMap K L) ζ
hcoe1 : (algebraMap (𝓞 K) L) ↑u = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
this : ((algebraMap K L) ζ - 1) ^ ↑p = 0 ∨ (aeval ((1 - ζ ^ m • α) / ((algebraMap K L) ζ - 1))) (poly hp hζ u hcong) = 0
⊢ (aeval ((1 - ζ ^ m • α) / ((algebraMap K L) ζ - 1))) (poly hp hζ u hcong) = 0
Theorem: KummersLemma.aeval_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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
m : ℕ
hζ' : (algebraMap K L) ζ - 1 ≠ 0
hcoe : (algebraMap (𝓞 K) L) ↑hζ.unit' = (algebraMap K L) ζ
hcoe1 : (algebraMap (𝓞 K) L) ↑u = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
this : ((algebraMap K L) ζ - 1) ^ ↑p = 0 ∨ (aeval ((1 - ζ ^ m • α) / ((algebraMap K L) ζ - 1))) (poly hp hζ u hcong) = 0
⊢ (aeval ((1 - ζ ^ m • α) / ((algebraMap K L) ζ - 1))) (poly hp hζ u hcong) = 0
Tactic:
exact this.resolve_left (pow_ne_zero _ hζ')
Proof state after:
no goals
Theorem: KummersLemma.aeval_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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
m : ℕ
⊢ (algebraMap K L) ζ - 1 ≠ 0
Tactic:
simpa using (algebraMap K L).injective.ne (hζ.sub_one_ne_zero hpri.out.one_lt)
Proof state after:
no goals
Theorem: KummersLemma.roots_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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
⊢ (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots =
    Multiset.map (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p).val
Tactic:
by_cases hα : α = 0
Proof state after:
case pos
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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hα : α = 0
⊢ (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots =
    Multiset.map (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p).val

case neg
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
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hα : ¬α = 0
⊢ (map (algebraMap (𝓞 K) L) (poly hp hζ u hcong)).roots =
    Multiset.map (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) (Finset.range ↑p).val