no goals
M : Type ?u.1452815
N : Type ?u.1452818
G : Type ?u.1452821
R : Type u_1
S : Type ?u.1452827
F : Type ?u.1452830
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
h : ζ ∈ primitiveRoots k R
hk : k = 0
⊢ IsPrimitiveRoot ζ k
simp [hk] at h