M : Type ?u.2907804
N : Type ?u.2907807
G : Type ?u.2907810
R : Type u_1
S : Type ?u.2907816
F : Type ?u.2907819
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
inst✝ : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
this : ↑i = ↑↑i
⊢ ↑(zmodEquivZpowers h) ↑i = ↑Additive.ofMul { val := ζ ^ i, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) ζ y = ζ ^ i) }
M : Type ?u.2907804
N : Type ?u.2907807
G : Type ?u.2907810
R : Type u_1
S : Type ?u.2907816
F : Type ?u.2907819
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
inst✝ : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
⊢ ↑(zmodEquivZpowers h) ↑i = ↑Additive.ofMul { val := ζ ^ i, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) ζ y = ζ ^ i) }
have : (i : ZMod k) = (i : ℤ) := by norm_cast
no goals
M : Type ?u.2907804
N : Type ?u.2907807
G : Type ?u.2907810
R : Type u_1
S : Type ?u.2907816
F : Type ?u.2907819
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
inst✝ : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
this : ↑i = ↑↑i
⊢ ↑(zmodEquivZpowers h) ↑i = ↑Additive.ofMul { val := ζ ^ i, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) ζ y = ζ ^ i) }
simp only [this, zmodEquivZpowers_apply_coe_int, zpow_ofNat]
no goals
M : Type ?u.2907804
N : Type ?u.2907807
G : Type ?u.2907810
R : Type u_1
S : Type ?u.2907816
F : Type ?u.2907819
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
inst✝ : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
⊢ ↑i = ↑↑i
norm_cast