M : Type u_1
N : Type ?u.2172208
G : Type ?u.2172211
R : Type ?u.2172214
S : Type ?u.2172217
F : Type ?u.2172220
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ k
⊢ orderOf (ζ ^ p) = k / p
M : Type u_1
N : Type ?u.2172208
G : Type ?u.2172211
R : Type ?u.2172214
S : Type ?u.2172217
F : Type ?u.2172220
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ k
⊢ IsPrimitiveRoot (ζ ^ p) (k / p)
suffices orderOf (ζ ^ p) = k / p by exact this ▸ IsPrimitiveRoot.orderOf (ζ ^ p)
no goals
M : Type u_1
N : Type ?u.2172208
G : Type ?u.2172211
R : Type ?u.2172214
S : Type ?u.2172217
F : Type ?u.2172220
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ k
⊢ orderOf (ζ ^ p) = k / p
rw [orderOf_pow' _ hp, ← eq_orderOf h, Nat.gcd_eq_right hdiv]
no goals
M : Type u_1
N : Type ?u.2172208
G : Type ?u.2172211
R : Type ?u.2172214
S : Type ?u.2172217
F : Type ?u.2172220
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ k
this : orderOf (ζ ^ p) = k / p
⊢ IsPrimitiveRoot (ζ ^ p) (k / p)
exact this ▸ IsPrimitiveRoot.orderOf (ζ ^ p)