case mp
M : Type ?u.3540580
N : Type ?u.3540583
G : Type ?u.3540586
R : Type u_1
S : Type ?u.3540592
F : Type ?u.3540595
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ
ζ ξ : R
h : IsPrimitiveRoot ζ k
h0 : 0 < k
⊢ IsPrimitiveRoot ξ k → ∃ i, i < k ∧ Nat.coprime i k ∧ ζ ^ i = ξ

case mpr
M : Type ?u.3540580
N : Type ?u.3540583
G : Type ?u.3540586
R : Type u_1
S : Type ?u.3540592
F : Type ?u.3540595
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ
ζ ξ : R
h : IsPrimitiveRoot ζ k
h0 : 0 < k
⊢ (∃ i, i < k ∧ Nat.coprime i k ∧ ζ ^ i = ξ) → IsPrimitiveRoot ξ k
M : Type ?u.3540580
N : Type ?u.3540583
G : Type ?u.3540586
R : Type u_1
S : Type ?u.3540592
F : Type ?u.3540595
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ
ζ ξ : R
h : IsPrimitiveRoot ζ k
h0 : 0 < k
⊢ IsPrimitiveRoot ξ k ↔ ∃ i, i < k ∧ Nat.coprime i k ∧ ζ ^ i = ξ
constructor
case mp
M : Type ?u.3540580
N : Type ?u.3540583
G : Type ?u.3540586
R : Type u_1
S : Type ?u.3540592
F : Type ?u.3540595
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ
ζ ξ : R
h : IsPrimitiveRoot ζ k
h0 : 0 < k
hξ : IsPrimitiveRoot ξ k
⊢ ∃ i, i < k ∧ Nat.coprime i k ∧ ζ ^ i = ξ
case mp
M : Type ?u.3540580
N : Type ?u.3540583
G : Type ?u.3540586
R : Type u_1
S : Type ?u.3540592
F : Type ?u.3540595
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ
ζ ξ : R
h : IsPrimitiveRoot ζ k
h0 : 0 < k
⊢ IsPrimitiveRoot ξ k → ∃ i, i < k ∧ Nat.coprime i k ∧ ζ ^ i = ξ
intro hξ
case mp.intro.intro
M : Type ?u.3540580
N : Type ?u.3540583
G : Type ?u.3540586
R : Type u_1
S : Type ?u.3540592
F : Type ?u.3540595
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ
ζ : R
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hik : i < k
hξ : IsPrimitiveRoot (ζ ^ i) k
⊢ ∃ i_1, i_1 < k ∧ Nat.coprime i_1 k ∧ ζ ^ i_1 = ζ ^ i
case mp
M : Type ?u.3540580
N : Type ?u.3540583
G : Type ?u.3540586
R : Type u_1
S : Type ?u.3540592
F : Type ?u.3540595
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ
ζ ξ : R
h : IsPrimitiveRoot ζ k
h0 : 0 < k
hξ : IsPrimitiveRoot ξ k
⊢ ∃ i, i < k ∧ Nat.coprime i k ∧ ζ ^ i = ξ
obtain ⟨i, hik, rfl⟩ := h.eq_pow_of_pow_eq_one hξ.pow_eq_one h0
case mp.intro.intro
M : Type ?u.3540580
N : Type ?u.3540583
G : Type ?u.3540586
R : Type u_1
S : Type ?u.3540592
F : Type ?u.3540595
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ
ζ : R
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hik : i < k
hξ : Nat.coprime i k
⊢ ∃ i_1, i_1 < k ∧ Nat.coprime i_1 k ∧ ζ ^ i_1 = ζ ^ i
case mp.intro.intro
M : Type ?u.3540580
N : Type ?u.3540583
G : Type ?u.3540586
R : Type u_1
S : Type ?u.3540592
F : Type ?u.3540595
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ
ζ : R
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hik : i < k
hξ : IsPrimitiveRoot (ζ ^ i) k
⊢ ∃ i_1, i_1 < k ∧ Nat.coprime i_1 k ∧ ζ ^ i_1 = ζ ^ i
rw [h.pow_iff_coprime h0] at hξ
no goals
case mp.intro.intro
M : Type ?u.3540580
N : Type ?u.3540583
G : Type ?u.3540586
R : Type u_1
S : Type ?u.3540592
F : Type ?u.3540595
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ
ζ : R
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hik : i < k
hξ : Nat.coprime i k
⊢ ∃ i_1, i_1 < k ∧ Nat.coprime i_1 k ∧ ζ ^ i_1 = ζ ^ i
exact ⟨i, hik, hξ, rfl⟩
case mpr.intro.intro.intro
M : Type ?u.3540580
N : Type ?u.3540583
G : Type ?u.3540586
R : Type u_1
S : Type ?u.3540592
F : Type ?u.3540595
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ
ζ : R
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : Nat.coprime i k
⊢ IsPrimitiveRoot (ζ ^ i) k
case mpr
M : Type ?u.3540580
N : Type ?u.3540583
G : Type ?u.3540586
R : Type u_1
S : Type ?u.3540592
F : Type ?u.3540595
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ
ζ ξ : R
h : IsPrimitiveRoot ζ k
h0 : 0 < k
⊢ (∃ i, i < k ∧ Nat.coprime i k ∧ ζ ^ i = ξ) → IsPrimitiveRoot ξ k
rintro ⟨i, -, hi, rfl⟩
no goals
case mpr.intro.intro.intro
M : Type ?u.3540580
N : Type ?u.3540583
G : Type ?u.3540586
R : Type u_1
S : Type ?u.3540592
F : Type ?u.3540595
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ
ζ : R
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : Nat.coprime i k
⊢ IsPrimitiveRoot (ζ ^ i) k
exact h.pow_of_coprime i hi