case mp
M : Type ?u.3462472
N : Type ?u.3462475
G : Type ?u.3462478
R : Type u_1
S : Type ?u.3462484
F : Type ?u.3462487
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
⊢ IsPrimitiveRoot ξ ↑k → ∃ i, i < ↑k ∧ Nat.coprime i ↑k ∧ ζ ^ i = ξ

case mpr
M : Type ?u.3462472
N : Type ?u.3462475
G : Type ?u.3462478
R : Type u_1
S : Type ?u.3462484
F : Type ?u.3462487
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
⊢ (∃ i, i < ↑k ∧ Nat.coprime i ↑k ∧ ζ ^ i = ξ) → IsPrimitiveRoot ξ ↑k
M : Type ?u.3462472
N : Type ?u.3462475
G : Type ?u.3462478
R : Type u_1
S : Type ?u.3462484
F : Type ?u.3462487
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
⊢ IsPrimitiveRoot ξ ↑k ↔ ∃ i, i < ↑k ∧ Nat.coprime i ↑k ∧ ζ ^ i = ξ
constructor
case mp
M : Type ?u.3462472
N : Type ?u.3462475
G : Type ?u.3462478
R : Type u_1
S : Type ?u.3462484
F : Type ?u.3462487
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
hξ : IsPrimitiveRoot ξ ↑k
⊢ ∃ i, i < ↑k ∧ Nat.coprime i ↑k ∧ ζ ^ i = ξ
case mp
M : Type ?u.3462472
N : Type ?u.3462475
G : Type ?u.3462478
R : Type u_1
S : Type ?u.3462484
F : Type ?u.3462487
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
⊢ IsPrimitiveRoot ξ ↑k → ∃ i, i < ↑k ∧ Nat.coprime i ↑k ∧ ζ ^ i = ξ
intro hξ
case mp.intro.intro
M : Type ?u.3462472
N : Type ?u.3462475
G : Type ?u.3462478
R : Type u_1
S : Type ?u.3462484
F : Type ?u.3462487
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
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.3462472
N : Type ?u.3462475
G : Type ?u.3462478
R : Type u_1
S : Type ?u.3462484
F : Type ?u.3462487
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
hξ : IsPrimitiveRoot ξ ↑k
⊢ ∃ i, i < ↑k ∧ Nat.coprime i ↑k ∧ ζ ^ i = ξ
obtain ⟨i, hik, rfl⟩ := h.eq_pow_of_mem_rootsOfUnity hξ.pow_eq_one
case mp.intro.intro
M : Type ?u.3462472
N : Type ?u.3462475
G : Type ?u.3462478
R : Type u_1
S : Type ?u.3462484
F : Type ?u.3462487
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
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.3462472
N : Type ?u.3462475
G : Type ?u.3462478
R : Type u_1
S : Type ?u.3462484
F : Type ?u.3462487
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
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 k.pos] at hξ
no goals
case mp.intro.intro
M : Type ?u.3462472
N : Type ?u.3462475
G : Type ?u.3462478
R : Type u_1
S : Type ?u.3462484
F : Type ?u.3462487
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
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.3462472
N : Type ?u.3462475
G : Type ?u.3462478
R : Type u_1
S : Type ?u.3462484
F : Type ?u.3462487
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
i : ℕ
hi : Nat.coprime i ↑k
⊢ IsPrimitiveRoot (ζ ^ i) ↑k
case mpr
M : Type ?u.3462472
N : Type ?u.3462475
G : Type ?u.3462478
R : Type u_1
S : Type ?u.3462484
F : Type ?u.3462487
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
⊢ (∃ i, i < ↑k ∧ Nat.coprime i ↑k ∧ ζ ^ i = ξ) → IsPrimitiveRoot ξ ↑k
rintro ⟨i, -, hi, rfl⟩
no goals
case mpr.intro.intro.intro
M : Type ?u.3462472
N : Type ?u.3462475
G : Type ?u.3462478
R : Type u_1
S : Type ?u.3462484
F : Type ?u.3462487
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
i : ℕ
hi : Nat.coprime i ↑k
⊢ IsPrimitiveRoot (ζ ^ i) ↑k
exact h.pow_of_coprime i hi