Theorem: KummersLemma.monic_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
⊢ (poly hp hζ u hcong).Monic
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
⊢ (poly hp hζ u hcong).Monic

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

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

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

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