Theorem: KummersLemma.irreducible_map_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
⊢ Irreducible (map (algebraMap (𝓞 K) K) (poly hp hζ u hcong))
Tactic:
rw [map_poly, ← irreducible_taylor_iff (r := 1 / (ζ - 1))]
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)))

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

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

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

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

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

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