no goals
R : Type u_2
G : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ↑f
⊢ IsCyclic G
classical
  cases nonempty_fintype G
  apply isCyclic_of_card_pow_eq_one_le
  intro n hn
  exact le_trans (card_nthRoots_subgroup_units f hf hn 1) (card_nthRoots n (f 1))
case intro
R : Type u_2
G : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ↑f
val✝ : Fintype G
⊢ IsCyclic G
R : Type u_2
G : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ↑f
⊢ IsCyclic G
cases nonempty_fintype G
case intro.hn
R : Type u_2
G : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ↑f
val✝ : Fintype G
⊢ ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
case intro
R : Type u_2
G : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ↑f
val✝ : Fintype G
⊢ IsCyclic G
apply isCyclic_of_card_pow_eq_one_le
case intro.hn
R : Type u_2
G : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ↑f
val✝ : Fintype G
n : ℕ
hn : 0 < n
⊢ card (filter (fun a => a ^ n = 1) univ) ≤ n
case intro.hn
R : Type u_2
G : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ↑f
val✝ : Fintype G
⊢ ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
intro n hn
no goals
case intro.hn
R : Type u_2
G : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ↑f
val✝ : Fintype G
n : ℕ
hn : 0 < n
⊢ card (filter (fun a => a ^ n = 1) univ) ≤ n
exact le_trans (card_nthRoots_subgroup_units f hf hn 1) (card_nthRoots n (f 1))