convert (hζ.powerBasis ℚ).lift_gen (S' := K) _ _
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
⊢ ((IsPrimitiveRoot.powerBasis ℚ ⋯).lift (IsPrimitiveRoot.powerBasis ℚ ⋯).gen ⋯) (zeta p ℚ K) = (zeta p ℚ K)⁻¹
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