Theorem: galConj_zeta_runity (FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean)

State before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ (galConj K p) ζ = ζ⁻¹
Tactic:
obtain ⟨t, _, rfl⟩ := (zeta_spec p ℚ K).eq_pow_of_pow_eq_one hζ.pow_eq_one p.pos
State after:
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)⁻¹

State before:
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)⁻¹
Tactic:
rw [map_pow, galConj_zeta, inv_pow]
State after:
no goals