Theorem: zeta_sub_one_pow_dvd_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
⊢ C ((↑hζ.unit' - 1) ^ ↑p) ∣ (C (↑hζ.unit' - 1) * X - 1) ^ ↑p + C ↑u
Tactic:
rw [← dvd_sub_left (_root_.map_dvd C hcong), add_sub_assoc, C.map_sub (u : 𝓞 K), ← sub_add,
  sub_self, map_one, zero_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
⊢ C ((↑hζ.unit' - 1) ^ ↑p) ∣ (C (↑hζ.unit' - 1) * X - 1) ^ ↑p + 1

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) ^ ↑p) ∣ (C (↑hζ.unit' - 1) * X - 1) ^ ↑p + 1
Tactic:
refine dvd_C_mul_X_sub_one_pow_add_one hpri.out (PNat.coe_injective.ne hp) _ _ dvd_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
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑↑p * (↑hζ.unit' - 1)

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
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑↑p * (↑hζ.unit' - 1)
Tactic:
conv_lhs => rw [← tsub_add_cancel_of_le (Nat.Prime.one_lt hpri.out).le, pow_succ]
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
⊢ (↑hζ.unit' - 1) ^ (↑p - 1) * (↑hζ.unit' - 1) ∣ ↑↑p * (↑hζ.unit' - 1)

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
⊢ (↑hζ.unit' - 1) ^ (↑p - 1) * (↑hζ.unit' - 1) ∣ ↑↑p * (↑hζ.unit' - 1)
Tactic:
exact mul_dvd_mul_right (associated_zeta_sub_one_pow_prime hζ).dvd _
State after:
no goals