α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
⊢ (fun x x_1 => x ^ x_1) (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α)))
      ↑(m / (Fintype.card α / Nat.gcd n (Fintype.card α))) =
    x
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : (fun x x_1 => x ^ x_1) g m = x
⊢ (fun x x_1 => x ^ x_1) (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α)))
      ↑(m / (Fintype.card α / Nat.gcd n (Fintype.card α))) =
    x
dsimp at hm
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1
⊢ (fun x x_1 => x ^ x_1) (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α)))
      ↑(m / (Fintype.card α / Nat.gcd n (Fintype.card α))) =
    x
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
⊢ (fun x x_1 => x ^ x_1) (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α)))
      ↑(m / (Fintype.card α / Nat.gcd n (Fintype.card α))) =
    x
have hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1 := by
  rw [pow_mul, hm, ← pow_gcd_card_eq_one_iff]; exact (mem_filter.1 hx).2
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1
⊢ (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α))) ^ ↑(m / (Fintype.card α / Nat.gcd n (Fintype.card α))) = x
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1
⊢ (fun x x_1 => x ^ x_1) (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α)))
      ↑(m / (Fintype.card α / Nat.gcd n (Fintype.card α))) =
    x
dsimp only
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1
⊢ Fintype.card α / Nat.gcd n (Fintype.card α) ∣ m
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1
⊢ (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α))) ^ ↑(m / (Fintype.card α / Nat.gcd n (Fintype.card α))) = x
rw [zpow_ofNat, ← pow_mul, Nat.mul_div_cancel_left', hm]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1
⊢ Fintype.card α / Nat.gcd n (Fintype.card α) * Nat.gcd n (Fintype.card α) ∣ m * Nat.gcd n (Fintype.card α)
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1
⊢ Fintype.card α / Nat.gcd n (Fintype.card α) ∣ m
refine' Nat.dvd_of_mul_dvd_mul_right (gcd_pos_of_pos_left (Fintype.card α) hn0) _
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1
⊢ orderOf g ∣ m * Nat.gcd n (Fintype.card α)
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1
⊢ Fintype.card α / Nat.gcd n (Fintype.card α) * Nat.gcd n (Fintype.card α) ∣ m * Nat.gcd n (Fintype.card α)
conv_lhs =>
  rw [Nat.div_mul_cancel (Nat.gcd_dvd_right _ _), ←
    orderOf_eq_card_of_forall_mem_zpowers hg]
no goals
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1
⊢ orderOf g ∣ m * Nat.gcd n (Fintype.card α)
exact orderOf_dvd_of_pow_eq_one hgmn
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
⊢ x ^ n = 1
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
⊢ g ^ (m * Nat.gcd n (Fintype.card α)) = 1
rw [pow_mul, hm, ← pow_gcd_card_eq_one_iff]
no goals
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
⊢ x ^ n = 1
exact (mem_filter.1 hx).2
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
⊢ card (Set.toFinset ↑(zpowers (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α))))) ≤ n
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
⊢ card (Set.toFinset ↑(zpowers (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α))))) ≤ n
let ⟨m, hm⟩ := Nat.gcd_dvd_right n (Fintype.card α)
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
hm0 : 0 < m
⊢ card (Set.toFinset ↑(zpowers (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α))))) ≤ n
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
⊢ card (Set.toFinset ↑(zpowers (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α))))) ≤ n
have hm0 : 0 < m :=
  Nat.pos_of_ne_zero fun hm0 => by
    rw [hm0, MulZeroClass.mul_zero, Fintype.card_eq_zero_iff] at hm
    exact hm.elim' 1
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
hm0 : 0 < m
⊢ Fintype.card { x // x ∈ zpowers (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α))) } ≤ n
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
hm0 : 0 < m
⊢ card (Set.toFinset ↑(zpowers (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α))))) ≤ n
simp only [Set.toFinset_card, SetLike.coe_sort_coe]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
hm0 : 0 < m
⊢ Fintype.card α / Nat.gcd (Fintype.card α) (Fintype.card α / Nat.gcd n (Fintype.card α)) ≤ n
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
hm0 : 0 < m
⊢ Fintype.card { x // x ∈ zpowers (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α))) } ≤ n
rw [← orderOf_eq_card_zpowers, orderOf_pow g, orderOf_eq_card_of_forall_mem_zpowers hg]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
hm0 : 0 < m
⊢ Fintype.card α / Nat.gcd (Nat.gcd n (Fintype.card α) * m) (Fintype.card α / Nat.gcd n (Fintype.card α)) ≤ n
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
hm0 : 0 < m
⊢ Fintype.card α / Nat.gcd (Fintype.card α) (Fintype.card α / Nat.gcd n (Fintype.card α)) ≤ n
nth_rw 2 [hm]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
hm0 : 0 < m
⊢ Fintype.card α /
      Nat.gcd (Nat.gcd n (Fintype.card α) * m) (Nat.gcd n (Fintype.card α) * m / Nat.gcd n (Fintype.card α)) ≤
    n
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
hm0 : 0 < m
⊢ Fintype.card α / Nat.gcd (Nat.gcd n (Fintype.card α) * m) (Fintype.card α / Nat.gcd n (Fintype.card α)) ≤ n
nth_rw 3 [hm]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
hm0 : 0 < m
⊢ Nat.gcd n (Fintype.card α) ≤ n
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
hm0 : 0 < m
⊢ Fintype.card α /
      Nat.gcd (Nat.gcd n (Fintype.card α) * m) (Nat.gcd n (Fintype.card α) * m / Nat.gcd n (Fintype.card α)) ≤
    n
rw [Nat.mul_div_cancel_left _ (gcd_pos_of_pos_left _ hn0), gcd_mul_left_left, hm,
  Nat.mul_div_cancel _ hm0]
no goals
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
hm0 : 0 < m
⊢ Nat.gcd n (Fintype.card α) ≤ n
exact le_of_dvd hn0 (Nat.gcd_dvd_left _ _)
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : IsEmpty α
hm0 : m = 0
⊢ False
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
hm0 : m = 0
⊢ False
rw [hm0, MulZeroClass.mul_zero, Fintype.card_eq_zero_iff] at hm
no goals
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : IsEmpty α
hm0 : m = 0
⊢ False
exact hm.elim' 1