Theorem: galConj_zeta (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) (zeta p ℚ K) = (zeta p ℚ K)⁻¹
Tactic:
let hζ := zeta_spec p ℚ K
State after:
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
⊢ (galConj K p) (zeta p ℚ K) = (zeta p ℚ K)⁻¹

State before:
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
⊢ (galConj K p) (zeta p ℚ K) = (zeta p ℚ K)⁻¹
Tactic:
simp only [galConj, Units.coe_neg_one, autEquivPow_symm_apply, AlgEquiv.coe_algHom,
  PowerBasis.equivOfMinpoly_apply]
State after:
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)⁻¹

State before:
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)⁻¹
Tactic:
convert (hζ.powerBasis ℚ).lift_gen (S' := K) _ _
State after:
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

State before:
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
Tactic:
rw [IsPrimitiveRoot.powerBasis_gen, ZMod.val_neg_one' p.pos,
  pow_sub₀ _ (hζ.ne_zero p.ne_zero) p.pos, pow_one, hζ.pow_eq_one, one_mul]
State after:
no goals