rw [map_pow, galConj_zeta, inv_pow]
case intro.intro
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
t : ℕ
left✝ : t < ↑p
hζ : IsPrimitiveRoot (zeta p ℚ K ^ t) ↑p
⊢ (galConj K p) (zeta p ℚ K ^ t) = (zeta p ℚ K ^ t)⁻¹
no goals