no goals
M : Type ?u.3141531
N : Type ?u.3141534
G : Type ?u.3141537
R : Type u_1
S : Type ?u.3141543
F : Type ?u.3141546
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
inst✝ : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
⊢ ↑(AddEquiv.symm (zmodEquivZpowers h))
      (↑Additive.ofMul { val := ζ ^ i, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) ζ y = ζ ^ i) }) =
    ↑i
rw [← h.zmodEquivZpowers.symm_apply_apply i, zmodEquivZpowers_apply_coe_nat]