M : Type u_1
N : Type ?u.2013558
G : Type ?u.2013561
R : Type ?u.2013564
S : Type ?u.2013567
F : Type ?u.2013570
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
⊢ IsPrimitiveRoot (ζ ^ i) k → Nat.coprime i k
M : Type u_1
N : Type ?u.2013558
G : Type ?u.2013561
R : Type ?u.2013564
S : Type ?u.2013567
F : Type ?u.2013570
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
⊢ IsPrimitiveRoot (ζ ^ i) k ↔ Nat.coprime i k
refine' ⟨_, h.pow_of_coprime i⟩
M : Type u_1
N : Type ?u.2013558
G : Type ?u.2013561
R : Type ?u.2013564
S : Type ?u.2013567
F : Type ?u.2013570
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : IsPrimitiveRoot (ζ ^ i) k
⊢ Nat.coprime i k
M : Type u_1
N : Type ?u.2013558
G : Type ?u.2013561
R : Type ?u.2013564
S : Type ?u.2013567
F : Type ?u.2013570
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
⊢ IsPrimitiveRoot (ζ ^ i) k → Nat.coprime i k
intro hi
case intro
M : Type u_1
N : Type ?u.2013558
G : Type ?u.2013561
R : Type ?u.2013564
S : Type ?u.2013567
F : Type ?u.2013570
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : IsPrimitiveRoot (ζ ^ i) k
a : ℕ
ha : i = Nat.gcd i k * a
⊢ Nat.coprime i k
M : Type u_1
N : Type ?u.2013558
G : Type ?u.2013561
R : Type ?u.2013564
S : Type ?u.2013567
F : Type ?u.2013570
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : IsPrimitiveRoot (ζ ^ i) k
⊢ Nat.coprime i k
obtain ⟨a, ha⟩ := i.gcd_dvd_left k
case intro.intro
M : Type u_1
N : Type ?u.2013558
G : Type ?u.2013561
R : Type ?u.2013564
S : Type ?u.2013567
F : Type ?u.2013570
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : IsPrimitiveRoot (ζ ^ i) k
a : ℕ
ha : i = Nat.gcd i k * a
b : ℕ
hb : k = Nat.gcd i k * b
⊢ Nat.coprime i k
case intro
M : Type u_1
N : Type ?u.2013558
G : Type ?u.2013561
R : Type ?u.2013564
S : Type ?u.2013567
F : Type ?u.2013570
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : IsPrimitiveRoot (ζ ^ i) k
a : ℕ
ha : i = Nat.gcd i k * a
⊢ Nat.coprime i k
obtain ⟨b, hb⟩ := i.gcd_dvd_right k
case intro.intro
M : Type u_1
N : Type ?u.2013558
G : Type ?u.2013561
R : Type ?u.2013564
S : Type ?u.2013567
F : Type ?u.2013570
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : IsPrimitiveRoot (ζ ^ i) k
a : ℕ
ha : i = Nat.gcd i k * a
b : ℕ
hb : k = Nat.gcd i k * b
⊢ b = k
case intro.intro
M : Type u_1
N : Type ?u.2013558
G : Type ?u.2013561
R : Type ?u.2013564
S : Type ?u.2013567
F : Type ?u.2013570
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : IsPrimitiveRoot (ζ ^ i) k
a : ℕ
ha : i = Nat.gcd i k * a
b : ℕ
hb : k = Nat.gcd i k * b
⊢ Nat.coprime i k
suffices b = k by
  rw [this, eq_comm, Nat.mul_left_eq_self_iff h0] at hb
  rwa [Nat.coprime]
case intro.intro
M : Type u_1
N : Type ?u.2013558
G : Type ?u.2013561
R : Type ?u.2013564
S : Type ?u.2013567
F : Type ?u.2013570
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
i a : ℕ
hi : IsPrimitiveRoot (ζ ^ (Nat.gcd i k * a)) k
ha : i = Nat.gcd i k * a
b : ℕ
hb : k = Nat.gcd i k * b
⊢ b = k
case intro.intro
M : Type u_1
N : Type ?u.2013558
G : Type ?u.2013561
R : Type ?u.2013564
S : Type ?u.2013567
F : Type ?u.2013570
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : IsPrimitiveRoot (ζ ^ i) k
a : ℕ
ha : i = Nat.gcd i k * a
b : ℕ
hb : k = Nat.gcd i k * b
⊢ b = k
rw [ha] at hi
case intro.intro
M : Type u_1
N : Type ?u.2013558
G : Type ?u.2013561
R : Type ?u.2013564
S : Type ?u.2013567
F : Type ?u.2013570
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
i a : ℕ
hi : IsPrimitiveRoot (ζ ^ (Nat.gcd i k * a)) k
ha : i = Nat.gcd i k * a
b : ℕ
hb : k = b * Nat.gcd i k
⊢ b = k
case intro.intro
M : Type u_1
N : Type ?u.2013558
G : Type ?u.2013561
R : Type ?u.2013564
S : Type ?u.2013567
F : Type ?u.2013570
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
i a : ℕ
hi : IsPrimitiveRoot (ζ ^ (Nat.gcd i k * a)) k
ha : i = Nat.gcd i k * a
b : ℕ
hb : k = Nat.gcd i k * b
⊢ b = k
rw [mul_comm] at hb
M : Type u_1
N : Type ?u.2013558
G : Type ?u.2013561
R : Type ?u.2013564
S : Type ?u.2013567
F : Type ?u.2013570
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
i a : ℕ
hi : IsPrimitiveRoot (ζ ^ (Nat.gcd i k * a)) k
ha : i = Nat.gcd i k * a
b : ℕ
hb : k = b * Nat.gcd i k
⊢ (ζ ^ (Nat.gcd i k * a)) ^ b = 1
case intro.intro
M : Type u_1
N : Type ?u.2013558
G : Type ?u.2013561
R : Type ?u.2013564
S : Type ?u.2013567
F : Type ?u.2013570
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
i a : ℕ
hi : IsPrimitiveRoot (ζ ^ (Nat.gcd i k * a)) k
ha : i = Nat.gcd i k * a
b : ℕ
hb : k = b * Nat.gcd i k
⊢ b = k
apply Nat.dvd_antisymm ⟨i.gcd k, hb⟩ (hi.dvd_of_pow_eq_one b _)
no goals
M : Type u_1
N : Type ?u.2013558
G : Type ?u.2013561
R : Type ?u.2013564
S : Type ?u.2013567
F : Type ?u.2013570
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
i a : ℕ
hi : IsPrimitiveRoot (ζ ^ (Nat.gcd i k * a)) k
ha : i = Nat.gcd i k * a
b : ℕ
hb : k = b * Nat.gcd i k
⊢ (ζ ^ (Nat.gcd i k * a)) ^ b = 1
rw [← pow_mul', ← mul_assoc, ← hb, pow_mul, h.pow_eq_one, one_pow]
M : Type u_1
N : Type ?u.2013558
G : Type ?u.2013561
R : Type ?u.2013564
S : Type ?u.2013567
F : Type ?u.2013570
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : IsPrimitiveRoot (ζ ^ i) k
a : ℕ
ha : i = Nat.gcd i k * a
b : ℕ
hb : Nat.gcd i k = 1
this : b = k
⊢ Nat.coprime i k
M : Type u_1
N : Type ?u.2013558
G : Type ?u.2013561
R : Type ?u.2013564
S : Type ?u.2013567
F : Type ?u.2013570
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : IsPrimitiveRoot (ζ ^ i) k
a : ℕ
ha : i = Nat.gcd i k * a
b : ℕ
hb : k = Nat.gcd i k * b
this : b = k
⊢ Nat.coprime i k
rw [this, eq_comm, Nat.mul_left_eq_self_iff h0] at hb
no goals
M : Type u_1
N : Type ?u.2013558
G : Type ?u.2013561
R : Type ?u.2013564
S : Type ?u.2013567
F : Type ?u.2013570
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : DivisionCommMonoid G
k l : ℕ
ζ : M
f : F
h✝ h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : IsPrimitiveRoot (ζ ^ i) k
a : ℕ
ha : i = Nat.gcd i k * a
b : ℕ
hb : Nat.gcd i k = 1
this : b = k
⊢ Nat.coprime i k
rwa [Nat.coprime]