rw [IsPrimitiveRoot.powerBasis_gen, ZMod.val_neg_one' p.pos,
  pow_sub₀ _ (hζ.ne_zero p.ne_zero) p.pos, pow_one, hζ.pow_eq_one, one_mul]
case h.e'_3
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑p
hζ : IsPrimitiveRoot (zeta p ℚ K) ↑p := zeta_spec p ℚ K
⊢ (zeta p ℚ K)⁻¹ = (IsPrimitiveRoot.powerBasis ℚ ⋯).gen
no goals