case pos
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : 0 ≤ l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l

case neg
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
⊢ ζ ^ l = 1 ↔ ↑k ∣ l
by_cases h0 : 0 ≤ l
case pos.intro
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
⊢ ζ ^ ↑l = 1 ↔ ↑k ∣ ↑l
case pos
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : 0 ≤ l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l
lift l to ℕ using h0
case pos.intro
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
⊢ ζ ^ l = 1 ↔ ↑k ∣ ↑l
case pos.intro
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
⊢ ζ ^ ↑l = 1 ↔ ↑k ∣ ↑l
rw [zpow_ofNat]
case pos.intro
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
⊢ ζ ^ l = 1 ↔ k ∣ l
case pos.intro
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
⊢ ζ ^ l = 1 ↔ ↑k ∣ ↑l
norm_cast
no goals
case pos.intro
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
⊢ ζ ^ l = 1 ↔ k ∣ l
exact h.pow_eq_one_iff_dvd l
case neg
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
this : 0 ≤ -l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l
case neg
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l
have : 0 ≤ -l := by simp only [not_le, neg_nonneg] at h0 ⊢; exact le_of_lt h0
case neg.intro
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : ↑l' = -l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l
case neg
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
this : 0 ≤ -l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l
lift -l to ℕ using this with l' hl'
case neg.intro
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : ↑l' = -l
⊢ ζ ^ l = 1 ↔ ↑k ∣ ↑l'
case neg.intro
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : ↑l' = -l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l
rw [← dvd_neg, ← hl']
case neg.intro
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : ↑l' = -l
⊢ ζ ^ l = 1 ↔ k ∣ l'
case neg.intro
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : ↑l' = -l
⊢ ζ ^ l = 1 ↔ ↑k ∣ ↑l'
norm_cast
no goals
case neg.intro
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : ↑l' = -l
⊢ ζ ^ l = 1 ↔ k ∣ l'
rw [← h.pow_eq_one_iff_dvd, ← inv_inj, ← zpow_neg, ← hl', zpow_ofNat, inv_one]
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : l < 0
⊢ l ≤ 0
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
⊢ 0 ≤ -l
simp only [not_le, neg_nonneg] at h0 ⊢
no goals
M : Type ?u.2651834
N : Type ?u.2651837
G : Type u_1
R : Type ?u.2651843
S : Type ?u.2651846
F : Type ?u.2651849
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l✝ : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : l < 0
⊢ l ≤ 0
exact le_of_lt h0