Theorem: KummersLemma.monic_poly_aux (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
⊢ ((C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u).leadingCoeff = (↑hζ.unit' - 1) ^ ↑p
Tactic:
haveI : Fact (Nat.Prime p) := hpri
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

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

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

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

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

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

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

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