Theorem: KummersLemma.aeval_poly (FltRegular/NumberTheory/KummersLemma/Field.lean)

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)
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

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]
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

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)
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

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
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

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
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

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
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

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
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

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ζ')
State after:
no goals

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)
State after:
no goals