no goals
M : Type u_1
N : Type ?u.1881352
G : Type ?u.1881355
R : Type ?u.1881358
S : Type ?u.1881361
F : Type ?u.1881364
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ✝ : M
f : F
h : IsPrimitiveRoot ζ✝ k
ζ : Mˣ
⊢ IsPrimitiveRoot (↑ζ) k ↔ IsPrimitiveRoot ζ k
simp only [iff_def, Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one]