Theorem: IsPrimitiveRoot.eq_one_mod_sub_of_pow (FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean)

State before:
p : ℕ+
K : Type ?u.65835
inst✝³ : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝² : NumberField K
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
ζ : A
hζ : IsPrimitiveRoot ζ ↑p
μ : A
hμ : μ ^ ↑p = 1
⊢ (algebraMap A (A ⧸ Ideal.span {ζ - 1})) μ = 1
Tactic:
obtain ⟨k, -, rfl⟩ := hζ.eq_pow_of_pow_eq_one hμ p.pos
State after:
case intro.intro
p : ℕ+
K : Type ?u.65835
inst✝³ : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝² : NumberField K
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
ζ : A
hζ : IsPrimitiveRoot ζ ↑p
k : ℕ
hμ : (ζ ^ k) ^ ↑p = 1
⊢ (algebraMap A (A ⧸ Ideal.span {ζ - 1})) (ζ ^ k) = 1

State before:
case intro.intro
p : ℕ+
K : Type ?u.65835
inst✝³ : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝² : NumberField K
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
ζ : A
hζ : IsPrimitiveRoot ζ ↑p
k : ℕ
hμ : (ζ ^ k) ^ ↑p = 1
⊢ (algebraMap A (A ⧸ Ideal.span {ζ - 1})) (ζ ^ k) = 1
Tactic:
rw [map_pow, eq_one_mod_one_sub, one_pow]
State after:
no goals