case intro
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
⊢ ∃ i, i < ↑k ∧ ζ ^ i = ζ ^ n
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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ξ : ξ ∈ rootsOfUnity k R
⊢ ∃ i, i < ↑k ∧ ζ ^ i = ξ
obtain ⟨n, rfl⟩ : ∃ n : ℤ, ζ ^ n = ξ := by rwa [← h.zpowers_eq] at hξ
case intro
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
hk0 : 0 < ↑↑k
⊢ ∃ i, i < ↑k ∧ ζ ^ i = ζ ^ n
case intro
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
⊢ ∃ i, i < ↑k ∧ ζ ^ i = ζ ^ n
have hk0 : (0 : ℤ) < k := by exact_mod_cast k.pos
case intro
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
hk0 : 0 < ↑↑k
i : ℤ := n % ↑↑k
⊢ ∃ i, i < ↑k ∧ ζ ^ i = ζ ^ n
case intro
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
hk0 : 0 < ↑↑k
⊢ ∃ i, i < ↑k ∧ ζ ^ i = ζ ^ n
let i := n % k
case intro
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
hk0 : 0 < ↑↑k
i : ℤ := n % ↑↑k
hi0 : 0 ≤ i
⊢ ∃ i, i < ↑k ∧ ζ ^ i = ζ ^ n
case intro
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
hk0 : 0 < ↑↑k
i : ℤ := n % ↑↑k
⊢ ∃ i, i < ↑k ∧ ζ ^ i = ζ ^ n
have hi0 : 0 ≤ i := Int.emod_nonneg _ (ne_of_gt hk0)
case intro.intro
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
hk0 : 0 < ↑↑k
i : ℤ := n % ↑↑k
i₀ : ℕ
hi₀ : ↑i₀ = i
⊢ ∃ i, i < ↑k ∧ ζ ^ i = ζ ^ n
case intro
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
hk0 : 0 < ↑↑k
i : ℤ := n % ↑↑k
hi0 : 0 ≤ i
⊢ ∃ i, i < ↑k ∧ ζ ^ i = ζ ^ n
lift i to ℕ using hi0 with i₀ hi₀
case intro.intro.refine'_1
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
hk0 : 0 < ↑↑k
i : ℤ := n % ↑↑k
i₀ : ℕ
hi₀ : ↑i₀ = i
⊢ i₀ < ↑k

case intro.intro.refine'_2
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
hk0 : 0 < ↑↑k
i : ℤ := n % ↑↑k
i₀ : ℕ
hi₀ : ↑i₀ = i
⊢ ζ ^ i₀ = ζ ^ n
case intro.intro
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
hk0 : 0 < ↑↑k
i : ℤ := n % ↑↑k
i₀ : ℕ
hi₀ : ↑i₀ = i
⊢ ∃ i, i < ↑k ∧ ζ ^ i = ζ ^ n
refine' ⟨i₀, _, _⟩
no goals
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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ξ : ξ ∈ rootsOfUnity k R
⊢ ∃ n, ζ ^ n = ξ
rwa [← h.zpowers_eq] at hξ
no goals
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
⊢ 0 < ↑↑k
exact_mod_cast k.pos
case intro.intro.refine'_1
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
hk0 : 0 < ↑↑k
i : ℤ := n % ↑↑k
i₀ : ℕ
hi₀ : ↑i₀ = i
⊢ ↑i₀ < ↑↑k
case intro.intro.refine'_1
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
hk0 : 0 < ↑↑k
i : ℤ := n % ↑↑k
i₀ : ℕ
hi₀ : ↑i₀ = i
⊢ i₀ < ↑k
zify
case intro.intro.refine'_1
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
hk0 : 0 < ↑↑k
i : ℤ := n % ↑↑k
i₀ : ℕ
hi₀ : ↑i₀ = i
⊢ i < ↑↑k
case intro.intro.refine'_1
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
hk0 : 0 < ↑↑k
i : ℤ := n % ↑↑k
i₀ : ℕ
hi₀ : ↑i₀ = i
⊢ ↑i₀ < ↑↑k
rw [hi₀]
no goals
case intro.intro.refine'_1
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
hk0 : 0 < ↑↑k
i : ℤ := n % ↑↑k
i₀ : ℕ
hi₀ : ↑i₀ = i
⊢ i < ↑↑k
exact Int.emod_lt_of_pos _ hk0
no goals
case intro.intro.refine'_2
M : Type ?u.3302393
N : Type ?u.3302396
G : Type ?u.3302399
R : Type u_1
S : Type ?u.3302405
F : Type ?u.3302408
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
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
hk0 : 0 < ↑↑k
i : ℤ := n % ↑↑k
i₀ : ℕ
hi₀ : ↑i₀ = i
⊢ ζ ^ i₀ = ζ ^ n
rw [← zpow_ofNat, hi₀, ← Int.emod_add_ediv n k, zpow_add, zpow_mul, h.zpow_eq_one, one_zpow,
  mul_one]