Theorem: IsPrimitiveRoot.unit'_pow (FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean)

State before:
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ hζ.unit' ^ ↑p = 1
Tactic:
ext
State after:
case a.h
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ ↑↑(hζ.unit' ^ ↑p) = ↑↑1

State before:
case a.h
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ ↑↑(hζ.unit' ^ ↑p) = ↑↑1
Tactic:
simpa using hζ.pow_eq_one
State after:
no goals