case pos
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : Int.gcd i ↑k = 1
h0 : 0 ≤ i
⊢ IsPrimitiveRoot (ζ ^ i) k

case neg
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : Int.gcd i ↑k = 1
h0 : ¬0 ≤ i
⊢ IsPrimitiveRoot (ζ ^ i) k
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : Int.gcd i ↑k = 1
⊢ IsPrimitiveRoot (ζ ^ i) k
by_cases h0 : 0 ≤ i
case neg
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : Int.gcd i ↑k = 1
h0 : ¬0 ≤ i
this : 0 ≤ -i
⊢ IsPrimitiveRoot (ζ ^ i) k
case neg
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : Int.gcd i ↑k = 1
h0 : ¬0 ≤ i
⊢ IsPrimitiveRoot (ζ ^ i) k
have : 0 ≤ -i := by simp only [not_le, neg_nonneg] at h0 ⊢; exact le_of_lt h0
case neg.intro
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : Int.gcd i ↑k = 1
h0 : ¬0 ≤ i
i' : ℕ
hi' : ↑i' = -i
⊢ IsPrimitiveRoot (ζ ^ i) k
case neg
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : Int.gcd i ↑k = 1
h0 : ¬0 ≤ i
this : 0 ≤ -i
⊢ IsPrimitiveRoot (ζ ^ i) k
lift -i to ℕ using this with i' hi'
case neg.intro
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : Int.gcd i ↑k = 1
h0 : ¬0 ≤ i
i' : ℕ
hi' : ↑i' = -i
⊢ IsPrimitiveRoot (ζ ^ i') k
case neg.intro
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : Int.gcd i ↑k = 1
h0 : ¬0 ≤ i
i' : ℕ
hi' : ↑i' = -i
⊢ IsPrimitiveRoot (ζ ^ i) k
rw [← inv_iff, ← zpow_neg, ← hi', zpow_ofNat]
case neg.intro.hi
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : Int.gcd i ↑k = 1
h0 : ¬0 ≤ i
i' : ℕ
hi' : ↑i' = -i
⊢ Nat.coprime i' k
case neg.intro
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : Int.gcd i ↑k = 1
h0 : ¬0 ≤ i
i' : ℕ
hi' : ↑i' = -i
⊢ IsPrimitiveRoot (ζ ^ i') k
apply h.pow_of_coprime
case neg.intro.hi
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
h0 : ¬0 ≤ i
i' : ℕ
hi : Nat.gcd (Int.natAbs ↑i') (Int.natAbs ↑k) = 1
hi' : ↑i' = -i
⊢ Nat.coprime i' k
case neg.intro.hi
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : Int.gcd i ↑k = 1
h0 : ¬0 ≤ i
i' : ℕ
hi' : ↑i' = -i
⊢ Nat.coprime i' k
rw [Int.gcd, ← Int.natAbs_neg, ← hi'] at hi
no goals
case neg.intro.hi
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
h0 : ¬0 ≤ i
i' : ℕ
hi : Nat.gcd (Int.natAbs ↑i') (Int.natAbs ↑k) = 1
hi' : ↑i' = -i
⊢ Nat.coprime i' k
exact hi
case pos.intro
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℕ
hi : Int.gcd ↑i ↑k = 1
⊢ IsPrimitiveRoot (ζ ^ ↑i) k
case pos
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : Int.gcd i ↑k = 1
h0 : 0 ≤ i
⊢ IsPrimitiveRoot (ζ ^ i) k
lift i to ℕ using h0
case pos.intro
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℕ
hi : Int.gcd ↑i ↑k = 1
⊢ IsPrimitiveRoot (ζ ^ i) k
case pos.intro
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℕ
hi : Int.gcd ↑i ↑k = 1
⊢ IsPrimitiveRoot (ζ ^ ↑i) k
rw [zpow_ofNat]
no goals
case pos.intro
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℕ
hi : Int.gcd ↑i ↑k = 1
⊢ IsPrimitiveRoot (ζ ^ i) k
exact h.pow_of_coprime i hi
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : Int.gcd i ↑k = 1
h0 : i < 0
⊢ i ≤ 0
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : Int.gcd i ↑k = 1
h0 : ¬0 ≤ i
⊢ 0 ≤ -i
simp only [not_le, neg_nonneg] at h0 ⊢
no goals
M : Type ?u.2707630
N : Type ?u.2707633
G : Type u_1
R : Type ?u.2707639
S : Type ?u.2707642
F : Type ?u.2707645
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : Int.gcd i ↑k = 1
h0 : i < 0
⊢ i ≤ 0
exact le_of_lt h0