M : Type u_1
N : Type ?u.2327355
G : Type ?u.2327358
R : Type ?u.2327361
S : Type ?u.2327364
F : Type ?u.2327367
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
⊢ IsPrimitiveRoot (ζ ^ a) b
M : Type u_1
N : Type ?u.2327355
G : Type ?u.2327358
R : Type ?u.2327361
S : Type ?u.2327364
F : Type ?u.2327367
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
n a b : ℕ
hn : 0 < n
h : IsPrimitiveRoot ζ n
hprod : n = a * b
⊢ IsPrimitiveRoot (ζ ^ a) b
subst n
M : Type u_1
N : Type ?u.2327355
G : Type ?u.2327358
R : Type ?u.2327361
S : Type ?u.2327364
F : Type ?u.2327367
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
⊢ ∀ (l : ℕ), ζ ^ (a * l) = 1 → b ∣ l
M : Type u_1
N : Type ?u.2327355
G : Type ?u.2327358
R : Type ?u.2327361
S : Type ?u.2327364
F : Type ?u.2327367
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
⊢ IsPrimitiveRoot (ζ ^ a) b
simp only [iff_def, ← pow_mul, h.pow_eq_one, eq_self_iff_true, true_and_iff]
M : Type u_1
N : Type ?u.2327355
G : Type ?u.2327358
R : Type ?u.2327361
S : Type ?u.2327364
F : Type ?u.2327367
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
l : ℕ
hl : ζ ^ (a * l) = 1
⊢ b ∣ l
M : Type u_1
N : Type ?u.2327355
G : Type ?u.2327358
R : Type ?u.2327361
S : Type ?u.2327364
F : Type ?u.2327367
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
⊢ ∀ (l : ℕ), ζ ^ (a * l) = 1 → b ∣ l
intro l hl
M : Type u_1
N : Type ?u.2327355
G : Type ?u.2327358
R : Type ?u.2327361
S : Type ?u.2327364
F : Type ?u.2327367
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
l : ℕ
hl : ζ ^ (a * l) = 1
ha0 : a ≠ 0
⊢ b ∣ l
M : Type u_1
N : Type ?u.2327355
G : Type ?u.2327358
R : Type ?u.2327361
S : Type ?u.2327364
F : Type ?u.2327367
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
l : ℕ
hl : ζ ^ (a * l) = 1
⊢ b ∣ l
have ha0 : a ≠ 0 := left_ne_zero_of_mul hn.ne'
M : Type u_1
N : Type ?u.2327355
G : Type ?u.2327358
R : Type ?u.2327361
S : Type ?u.2327364
F : Type ?u.2327367
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
l : ℕ
hl : ζ ^ (a * l) = 1
ha0 : a ≠ 0
⊢ a * b ∣ a * l
M : Type u_1
N : Type ?u.2327355
G : Type ?u.2327358
R : Type ?u.2327361
S : Type ?u.2327364
F : Type ?u.2327367
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
l : ℕ
hl : ζ ^ (a * l) = 1
ha0 : a ≠ 0
⊢ b ∣ l
rw [← mul_dvd_mul_iff_left ha0]
no goals
M : Type u_1
N : Type ?u.2327355
G : Type ?u.2327358
R : Type ?u.2327361
S : Type ?u.2327364
F : Type ?u.2327367
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
f : F
h✝ : IsPrimitiveRoot ζ k
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
l : ℕ
hl : ζ ^ (a * l) = 1
ha0 : a ≠ 0
⊢ a * b ∣ a * l
exact h.dvd_of_pow_eq_one _ hl