rw [← Complex.abs_mul_exp_arg_mul_I x, h, Complex.ofReal_one, one_mul, ← Complex.exp_conj, ←
  Complex.exp_neg, map_mul, Complex.conj_I, mul_neg, Complex.conj_ofReal]
K : Type ?u.24099
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x : ℂ
h : Complex.abs x = 1
⊢ (starRingEnd ℂ) x = x⁻¹
no goals