M : Type u_1
N : Type ?u.1556454
G : Type ?u.1556457
R : Type ?u.1556460
S : Type ?u.1556463
F : Type ?u.1556466
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
⊢ k ∣ l
M : Type u_1
N : Type ?u.1556454
G : Type ?u.1556457
R : Type ?u.1556460
S : Type ?u.1556463
F : Type ?u.1556466
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
⊢ IsPrimitiveRoot ζ k
refine' ⟨h1, fun l hl => _⟩
M : Type u_1
N : Type ?u.1556454
G : Type ?u.1556457
R : Type ?u.1556460
S : Type ?u.1556463
F : Type ?u.1556466
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
⊢ Nat.gcd k l = k
M : Type u_1
N : Type ?u.1556454
G : Type ?u.1556457
R : Type ?u.1556460
S : Type ?u.1556463
F : Type ?u.1556466
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
⊢ k ∣ l
suffices k.gcd l = k by exact this ▸ k.gcd_dvd_right l
M : Type u_1
N : Type ?u.1556454
G : Type ?u.1556457
R : Type ?u.1556460
S : Type ?u.1556463
F : Type ?u.1556466
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
⊢ Nat.gcd k l ≤ k ∧ ¬Nat.gcd k l < k
M : Type u_1
N : Type ?u.1556454
G : Type ?u.1556457
R : Type ?u.1556460
S : Type ?u.1556463
F : Type ?u.1556466
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
⊢ Nat.gcd k l = k
rw [eq_iff_le_not_lt]
M : Type u_1
N : Type ?u.1556454
G : Type ?u.1556457
R : Type ?u.1556460
S : Type ?u.1556463
F : Type ?u.1556466
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
⊢ ¬Nat.gcd k l < k
M : Type u_1
N : Type ?u.1556454
G : Type ?u.1556457
R : Type ?u.1556460
S : Type ?u.1556463
F : Type ?u.1556466
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
⊢ Nat.gcd k l ≤ k ∧ ¬Nat.gcd k l < k
refine' ⟨Nat.le_of_dvd hk (k.gcd_dvd_left l), _⟩
M : Type u_1
N : Type ?u.1556454
G : Type ?u.1556457
R : Type ?u.1556460
S : Type ?u.1556463
F : Type ?u.1556466
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
h' : Nat.gcd k l < k
⊢ False
M : Type u_1
N : Type ?u.1556454
G : Type ?u.1556457
R : Type ?u.1556460
S : Type ?u.1556463
F : Type ?u.1556466
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
⊢ ¬Nat.gcd k l < k
intro h'
M : Type u_1
N : Type ?u.1556454
G : Type ?u.1556457
R : Type ?u.1556460
S : Type ?u.1556463
F : Type ?u.1556466
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
h' : Nat.gcd k l < k
⊢ ζ ^ Nat.gcd k l = 1
M : Type u_1
N : Type ?u.1556454
G : Type ?u.1556457
R : Type ?u.1556460
S : Type ?u.1556463
F : Type ?u.1556466
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
h' : Nat.gcd k l < k
⊢ False
apply h _ (Nat.gcd_pos_of_pos_left _ hk) h'
no goals
M : Type u_1
N : Type ?u.1556454
G : Type ?u.1556457
R : Type ?u.1556460
S : Type ?u.1556463
F : Type ?u.1556466
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
h' : Nat.gcd k l < k
⊢ ζ ^ Nat.gcd k l = 1
exact pow_gcd_eq_one _ h1 hl
no goals
M : Type u_1
N : Type ?u.1556454
G : Type ?u.1556457
R : Type ?u.1556460
S : Type ?u.1556463
F : Type ?u.1556466
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
this : Nat.gcd k l = k
⊢ k ∣ l
exact this ▸ k.gcd_dvd_right l