rwa [natDegree_C_mul, natDegree_poly_aux hζ] at this
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
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