no goals
M : Type u_2
N : Type u_3
G : Type ?u.2380264
R : Type ?u.2380267
S : Type ?u.2380270
F : Type u_1
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ↑f
⊢ ↑f ζ ^ k = 1
rw [← map_pow, h.pow_eq_one, _root_.map_one]
M : Type u_2
N : Type u_3
G : Type ?u.2380264
R : Type ?u.2380267
S : Type ?u.2380270
F : Type u_1
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ↑f
⊢ ∀ (l : ℕ), ↑f ζ ^ l = 1 → orderOf ζ ∣ l
M : Type u_2
N : Type u_3
G : Type ?u.2380264
R : Type ?u.2380267
S : Type ?u.2380270
F : Type u_1
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ↑f
⊢ ∀ (l : ℕ), ↑f ζ ^ l = 1 → k ∣ l
rw [h.eq_orderOf]
M : Type u_2
N : Type u_3
G : Type ?u.2380264
R : Type ?u.2380267
S : Type ?u.2380270
F : Type u_1
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ↑f
l : ℕ
hl : ↑f ζ ^ l = 1
⊢ orderOf ζ ∣ l
M : Type u_2
N : Type u_3
G : Type ?u.2380264
R : Type ?u.2380267
S : Type ?u.2380270
F : Type u_1
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ↑f
⊢ ∀ (l : ℕ), ↑f ζ ^ l = 1 → orderOf ζ ∣ l
intro l hl
M : Type u_2
N : Type u_3
G : Type ?u.2380264
R : Type ?u.2380267
S : Type ?u.2380270
F : Type u_1
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ↑f
l : ℕ
hl : ↑f (ζ ^ l) = ↑f 1
⊢ orderOf ζ ∣ l
M : Type u_2
N : Type u_3
G : Type ?u.2380264
R : Type ?u.2380267
S : Type ?u.2380270
F : Type u_1
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ↑f
l : ℕ
hl : ↑f ζ ^ l = 1
⊢ orderOf ζ ∣ l
rw [← map_pow, ← map_one f] at hl
no goals
M : Type u_2
N : Type u_3
G : Type ?u.2380264
R : Type ?u.2380267
S : Type ?u.2380270
F : Type u_1
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ↑f
l : ℕ
hl : ↑f (ζ ^ l) = ↑f 1
⊢ orderOf ζ ∣ l
exact orderOf_dvd_of_pow_eq_one (hf hl)