Theorem: galConj_idempotent (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).trans (galConj K p) = AlgEquiv.refl
Tactic:
rw [← AlgEquiv.aut_mul, galConj, ← map_mul, neg_one_mul, neg_neg, map_one]
State after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ 1 = AlgEquiv.refl

State before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ 1 = AlgEquiv.refl
Tactic:
rfl
State after:
no goals