internlm/Lean-Github huggingface dataset:
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
this : Fact (↑p).Prime
⊢ (poly hp hζ u hcong).Monic
Tactic:
have := congr_arg leadingCoeff (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
this✝ : Fact (↑p).Prime
this :
  (C ((↑hζ.unit' - 1) ^ ↑p) * poly hp hζ u hcong).leadingCoeff = ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).leadingCoeff
⊢ (poly hp hζ u hcong).Monic
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
this✝ : Fact (↑p).Prime
this :
  (C ((↑hζ.unit' - 1) ^ ↑p) * poly hp hζ u hcong).leadingCoeff = ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).leadingCoeff
⊢ (poly hp hζ u hcong).Monic
Tactic:
simp only [map_pow, leadingCoeff_mul, leadingCoeff_pow, leadingCoeff_C, ne_eq, PNat.pos,
  pow_eq_zero_iff, monic_poly_aux hζ] 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
this✝ : Fact (↑p).Prime
this : (↑hζ.unit' - 1) ^ ↑p * (poly hp hζ u hcong).leadingCoeff = (↑hζ.unit' - 1) ^ ↑p
⊢ (poly hp hζ u hcong).Monic
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
this✝ : Fact (↑p).Prime
this : (↑hζ.unit' - 1) ^ ↑p * (poly hp hζ u hcong).leadingCoeff = (↑hζ.unit' - 1) ^ ↑p
⊢ (poly hp hζ u hcong).Monic
Tactic:
refine mul_right_injective₀ ?_ (this.trans (mul_one _).symm)
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
this : (↑hζ.unit' - 1) ^ ↑p * (poly hp hζ u hcong).leadingCoeff = (↑hζ.unit' - 1) ^ ↑p
⊢ (↑hζ.unit' - 1) ^ ↑p ≠ 0
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
this✝ : Fact (↑p).Prime
this : (↑hζ.unit' - 1) ^ ↑p * (poly hp hζ u hcong).leadingCoeff = (↑hζ.unit' - 1) ^ ↑p
⊢ (↑hζ.unit' - 1) ^ ↑p ≠ 0
Tactic:
exact pow_ne_zero _ (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt)
Proof state after:
no goals
Theorem: KummersLemma.natDegree_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).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
⊢ (poly hp hζ u hcong).natDegree = ↑p
Theorem: KummersLemma.natDegree_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
this : Fact (↑p).Prime
⊢ (poly hp hζ u hcong).natDegree = ↑p
Tactic:
have := congr_arg natDegree (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
this✝ : Fact (↑p).Prime
this : (C ((↑hζ.unit' - 1) ^ ↑p) * poly hp hζ u hcong).natDegree = ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).natDegree
⊢ (poly hp hζ u hcong).natDegree = ↑p
Theorem: KummersLemma.natDegree_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
this✝ : Fact (↑p).Prime
this : (C ((↑hζ.unit' - 1) ^ ↑p) * poly hp hζ u hcong).natDegree = ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).natDegree
⊢ (poly hp hζ u hcong).natDegree = ↑p
Tactic:
rwa [natDegree_C_mul, natDegree_poly_aux hζ] 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
this✝ : Fact (↑p).Prime
this : (C ((↑hζ.unit' - 1) ^ ↑p) * poly hp hζ u hcong).natDegree = ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).natDegree
⊢ (↑hζ.unit' - 1) ^ ↑p ≠ 0
Theorem: KummersLemma.natDegree_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
this✝ : Fact (↑p).Prime
this : (C ((↑hζ.unit' - 1) ^ ↑p) * poly hp hζ u hcong).natDegree = ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).natDegree
⊢ (↑hζ.unit' - 1) ^ ↑p ≠ 0
Tactic:
exact pow_ne_zero _ (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt)
Proof state after:
no goals
Theorem: KummersLemma.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
⊢ map (algebraMap (𝓞 K) K) (poly hp hζ u hcong) =
    (X - C (1 / (ζ - 1))) ^ ↑p + C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)
Tactic:
ext i
Proof state after:
case 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 : ℕ
⊢ (map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i =
    ((X - C (1 / (ζ - 1))) ^ ↑p + C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)).coeff i
Theorem: KummersLemma.map_poly
Proof state before:
case 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 : ℕ
⊢ (map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i =
    ((X - C (1 / (ζ - 1))) ^ ↑p + C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)).coeff i
Tactic:
have := congr_arg (fun P : (𝓞 K)[X] ↦ (↑(coeff P i) : K)) (poly_spec hp hζ u hcong)
Proof state after:
case 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 :
  (fun P => ↑(P.coeff i)) (C ((↑hζ.unit' - 1) ^ ↑p) * poly hp hζ u hcong) =
    (fun P => ↑(P.coeff i)) ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u)
⊢ (map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i =
    ((X - C (1 / (ζ - 1))) ^ ↑p + C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)).coeff i
Theorem: KummersLemma.map_poly
Proof state before:
case 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 :
  (fun P => ↑(P.coeff i)) (C ((↑hζ.unit' - 1) ^ ↑p) * poly hp hζ u hcong) =
    (fun P => ↑(P.coeff i)) ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u)
⊢ (map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i =
    ((X - C (1 / (ζ - 1))) ^ ↑p + C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)).coeff i
Tactic:
change _ = algebraMap (𝓞 K) K _ at this
Proof state after:
case 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 :
  (fun P => ↑(P.coeff i)) (C ((↑hζ.unit' - 1) ^ ↑p) * poly hp hζ u hcong) =
    (algebraMap (𝓞 K) K) (((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).coeff i)
⊢ (map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i =
    ((X - C (1 / (ζ - 1))) ^ ↑p + C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)).coeff i
Theorem: KummersLemma.map_poly
Proof state before:
case 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 :
  (fun P => ↑(P.coeff i)) (C ((↑hζ.unit' - 1) ^ ↑p) * poly hp hζ u hcong) =
    (algebraMap (𝓞 K) K) (((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).coeff i)
⊢ (map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i =
    ((X - C (1 / (ζ - 1))) ^ ↑p + C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)).coeff i
Tactic:
rw [← coeff_map] at this
Proof state after:
case 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 :
  (fun P => ↑(P.coeff i)) (C ((↑hζ.unit' - 1) ^ ↑p) * poly hp hζ u hcong) =
    (map (algebraMap (𝓞 K) K) ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u)).coeff i
⊢ (map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i =
    ((X - C (1 / (ζ - 1))) ^ ↑p + C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)).coeff i
Theorem: KummersLemma.map_poly
Proof state before:
case 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 :
  (fun P => ↑(P.coeff i)) (C ((↑hζ.unit' - 1) ^ ↑p) * poly hp hζ u hcong) =
    (map (algebraMap (𝓞 K) K) ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u)).coeff i
⊢ (map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i =
    ((X - C (1 / (ζ - 1))) ^ ↑p + C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)).coeff i
Tactic:
replace 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 := by
    simp only [map_pow, map_sub, map_one, Polynomial.map_add, Polynomial.map_pow,
      Polynomial.map_sub, Polynomial.map_mul, map_C, IsPrimitiveRoot.coe_unit'_coe,
      Polynomial.map_one, map_X, coeff_add] at this
    convert this
    simp only [NumberField.RingOfIntegers.coe_eq_algebraMap, ← Polynomial.coeff_map]
    simp only [coeff_map, Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_sub, map_C,
      IsPrimitiveRoot.coe_unit'_coe, Polynomial.map_one]
    rw [← Polynomial.coeff_map, mul_comm, ← Polynomial.coeff_mul_C, mul_comm]
    simp
Proof state after:
case 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
⊢ (map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i =
    ((X - C (1 / (ζ - 1))) ^ ↑p + C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)).coeff i
Theorem: KummersLemma.map_poly
Proof state before:
case 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
⊢ (map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i =
    ((X - C (1 / (ζ - 1))) ^ ↑p + C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)).coeff i
Tactic:
apply mul_right_injective₀ (pow_ne_zero p (hζ.sub_one_ne_zero hpri.out.one_lt))
Proof state after:
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
⊢ (fun x => (ζ - 1) ^ ↑p * x) ((map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i) =
    (fun x => (ζ - 1) ^ ↑p * x) (((X - C (1 / (ζ - 1))) ^ ↑p + C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)).coeff i)
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
⊢ (fun x => (ζ - 1) ^ ↑p * x) ((map (algebraMap (𝓞 K) K) (poly hp hζ u hcong)).coeff i) =
    (fun x => (ζ - 1) ^ ↑p * x) (((X - C (1 / (ζ - 1))) ^ ↑p + C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)).coeff i)
Tactic:
simp only [Subalgebra.algebraMap_eq, Algebra.id.map_eq_id, RingHomCompTriple.comp_eq, coeff_map,
  RingHom.coe_coe, Subalgebra.coe_val, one_div, map_sub, map_one, coeff_add, coeff_sub,
  PNat.pos, pow_eq_zero_iff, this, mul_add, IsPrimitiveRoot.val_unit'_coe,
  IsPrimitiveRoot.coe_unit'_coe]
Proof state after:
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
⊢ (((C ζ - 1) * X - 1) ^ ↑p).coeff i + (C ((algebraMap (𝓞 K) K) ↑u)).coeff i =
    (ζ - 1) ^ ↑p * ((X - C (ζ - 1)⁻¹) ^ ↑p).coeff i +
      (ζ - 1) ^ ↑p * (C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)).coeff i
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
⊢ (((C ζ - 1) * X - 1) ^ ↑p).coeff i + (C ((algebraMap (𝓞 K) K) ↑u)).coeff i =
    (ζ - 1) ^ ↑p * ((X - C (ζ - 1)⁻¹) ^ ↑p).coeff i +
      (ζ - 1) ^ ↑p * (C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)).coeff i
Tactic:
simp_rw [← smul_eq_mul K, ← coeff_smul]
Proof state after:
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
⊢ (((C ζ - 1) * X - 1) ^ ↑p).coeff i + (C ((algebraMap (𝓞 K) K) ↑u)).coeff i =
    ((ζ - 1) ^ ↑p • (X - C (ζ - 1)⁻¹) ^ ↑p).coeff i +
      ((ζ - 1) ^ ↑p • C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)).coeff i
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
⊢ (((C ζ - 1) * X - 1) ^ ↑p).coeff i + (C ((algebraMap (𝓞 K) K) ↑u)).coeff i =
    ((ζ - 1) ^ ↑p • (X - C (ζ - 1)⁻¹) ^ ↑p).coeff i +
      ((ζ - 1) ^ ↑p • C ((algebraMap (𝓞 K) K) ↑u / (ζ - 1) ^ ↑p)).coeff i
Tactic:
rw [smul_C, smul_eq_mul, ← smul_pow, ← mul_div_assoc, mul_div_cancel_left₀, smul_sub, smul_C,
  smul_eq_mul, mul_inv_cancel, map_one, Algebra.smul_def, ← C_eq_algebraMap, map_sub, map_one]
Proof state after:
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

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
Theorem: KummersLemma.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
i : ℕ
this :
  (fun P => ↑(P.coeff i)) (C ((↑hζ.unit' - 1) ^ ↑p) * poly hp hζ u hcong) =
    (map (algebraMap (𝓞 K) K) ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u)).coeff i
⊢ (ζ - 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
Tactic:
simp only [map_pow, map_sub, map_one, Polynomial.map_add, Polynomial.map_pow,
  Polynomial.map_sub, Polynomial.map_mul, map_C, IsPrimitiveRoot.coe_unit'_coe,
  Polynomial.map_one, map_X, coeff_add] 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
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 * ↑((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
Theorem: KummersLemma.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
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 * ↑((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
Tactic:
convert this
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 * ↑((poly hp hζ u hcong).coeff i) = ↑(((C ↑hζ.unit' - 1) ^ ↑p * 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 * ↑((poly hp hζ u hcong).coeff i) = ↑(((C ↑hζ.unit' - 1) ^ ↑p * poly hp hζ u hcong).coeff i)
Tactic:
simp only [NumberField.RingOfIntegers.coe_eq_algebraMap, ← Polynomial.coeff_map]
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 * (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