case intro
M : Type ?u.3458904
N : Type ?u.3458907
G : Type ?u.3458910
R : Type u_1
S : Type ?u.3458916
F : Type ?u.3458919
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ
ξ : R
hξ : ξ ^ k = 1
h0 : 0 < k
ζ : Rˣ
h : IsPrimitiveRoot (↑ζ) k
⊢ ∃ i, i < k ∧ ↑ζ ^ i = ξ
M : Type ?u.3458904
N : Type ?u.3458907
G : Type ?u.3458910
R : Type u_1
S : Type ?u.3458916
F : Type ?u.3458919
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ξ : ξ ^ k = 1
h0 : 0 < k
⊢ ∃ i, i < k ∧ ζ ^ i = ξ
lift ζ to Rˣ using h.isUnit h0
case intro.intro
M : Type ?u.3458904
N : Type ?u.3458907
G : Type ?u.3458910
R : Type u_1
S : Type ?u.3458916
F : Type ?u.3458919
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ
h0 : 0 < k
ζ : Rˣ
h : IsPrimitiveRoot (↑ζ) k
ξ : Rˣ
hξ : ↑ξ ^ k = 1
⊢ ∃ i, i < k ∧ ↑ζ ^ i = ↑ξ
case intro
M : Type ?u.3458904
N : Type ?u.3458907
G : Type ?u.3458910
R : Type u_1
S : Type ?u.3458916
F : Type ?u.3458919
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ
ξ : R
hξ : ξ ^ k = 1
h0 : 0 < k
ζ : Rˣ
h : IsPrimitiveRoot (↑ζ) k
⊢ ∃ i, i < k ∧ ↑ζ ^ i = ξ
lift ξ to Rˣ using isUnit_ofPowEqOne hξ h0.ne'
case intro.intro.intro
M : Type ?u.3458904
N : Type ?u.3458907
G : Type ?u.3458910
R : Type u_1
S : Type ?u.3458916
F : Type ?u.3458919
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ ξ : Rˣ
k : ℕ+
h : IsPrimitiveRoot ↑ζ ↑k
hξ : ↑ξ ^ ↑k = 1
⊢ ∃ i, i < ↑k ∧ ↑ζ ^ i = ↑ξ
case intro.intro
M : Type ?u.3458904
N : Type ?u.3458907
G : Type ?u.3458910
R : Type u_1
S : Type ?u.3458916
F : Type ?u.3458919
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ
h0 : 0 < k
ζ : Rˣ
h : IsPrimitiveRoot (↑ζ) k
ξ : Rˣ
hξ : ↑ξ ^ k = 1
⊢ ∃ i, i < k ∧ ↑ζ ^ i = ↑ξ
lift k to ℕ+ using h0
case intro.intro.intro
M : Type ?u.3458904
N : Type ?u.3458907
G : Type ?u.3458910
R : Type u_1
S : Type ?u.3458916
F : Type ?u.3458919
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ ξ : Rˣ
k : ℕ+
h : IsPrimitiveRoot ↑ζ ↑k
hξ : ↑ξ ^ ↑k = 1
⊢ ∃ i, i < ↑k ∧ ζ ^ i = ξ
case intro.intro.intro
M : Type ?u.3458904
N : Type ?u.3458907
G : Type ?u.3458910
R : Type u_1
S : Type ?u.3458916
F : Type ?u.3458919
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ ξ : Rˣ
k : ℕ+
h : IsPrimitiveRoot ↑ζ ↑k
hξ : ↑ξ ^ ↑k = 1
⊢ ∃ i, i < ↑k ∧ ↑ζ ^ i = ↑ξ
simp only [← Units.val_pow_eq_pow_val, ← Units.ext_iff]
case intro.intro.intro
M : Type ?u.3458904
N : Type ?u.3458907
G : Type ?u.3458910
R : Type u_1
S : Type ?u.3458916
F : Type ?u.3458919
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ ξ : Rˣ
k : ℕ+
h : IsPrimitiveRoot ζ ↑k
hξ : ↑ξ ^ ↑k = 1
⊢ ∃ i, i < ↑k ∧ ζ ^ i = ξ
case intro.intro.intro
M : Type ?u.3458904
N : Type ?u.3458907
G : Type ?u.3458910
R : Type u_1
S : Type ?u.3458916
F : Type ?u.3458919
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ ξ : Rˣ
k : ℕ+
h : IsPrimitiveRoot ↑ζ ↑k
hξ : ↑ξ ^ ↑k = 1
⊢ ∃ i, i < ↑k ∧ ζ ^ i = ξ
rw [coe_units_iff] at h
case intro.intro.intro
M : Type ?u.3458904
N : Type ?u.3458907
G : Type ?u.3458910
R : Type u_1
S : Type ?u.3458916
F : Type ?u.3458919
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ ξ : Rˣ
k : ℕ+
h : IsPrimitiveRoot ζ ↑k
hξ : ↑ξ ^ ↑k = 1
⊢ ξ ∈ rootsOfUnity k R
case intro.intro.intro
M : Type ?u.3458904
N : Type ?u.3458907
G : Type ?u.3458910
R : Type u_1
S : Type ?u.3458916
F : Type ?u.3458919
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ ξ : Rˣ
k : ℕ+
h : IsPrimitiveRoot ζ ↑k
hξ : ↑ξ ^ ↑k = 1
⊢ ∃ i, i < ↑k ∧ ζ ^ i = ξ
apply h.eq_pow_of_mem_rootsOfUnity
no goals
case intro.intro.intro
M : Type ?u.3458904
N : Type ?u.3458907
G : Type ?u.3458910
R : Type u_1
S : Type ?u.3458916
F : Type ?u.3458919
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ ξ : Rˣ
k : ℕ+
h : IsPrimitiveRoot ζ ↑k
hξ : ↑ξ ^ ↑k = 1
⊢ ξ ∈ rootsOfUnity k R
rw [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val, hξ, Units.val_one]