Commit 2024-05-30 13:23 db99aaa2

feat(RingTheory/RootsOfUnity/Basic): add more covenient version of a lemma (#13375) This provides

lemma eq_pow_of_mem_rootsOfUnity' {k : ℕ} (hk : 0 < k) {ζ : R} (hζ : IsPrimitiveRoot ζ k) {ξ : Rˣ}
    (hξ : ξ ∈ rootsOfUnity (⟨k, hk⟩ : ℕ+) R) : ∃ i < k, ζ ^ i = ξ

for ease of use compared with IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity, which requires k to be a PNat and ζ to be a unit.