case mk.intro
α✝ : Type u
a : α✝
inst✝⁵ : Group α✝
inst✝⁴ : DecidableEq α✝
inst✝³ : Fintype α✝
hn✝ : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => n • a = 0) univ) ≤ n
g : Multiplicative α
hg : ∀ (x : Multiplicative α), x ∈ zpowers g
⊢ IsAddCyclic α
α✝ : Type u
a : α✝
inst✝⁵ : Group α✝
inst✝⁴ : DecidableEq α✝
inst✝³ : Fintype α✝
hn✝ : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => n • a = 0) univ) ≤ n
⊢ IsAddCyclic α
obtain ⟨g, hg⟩ := (@isCyclic_of_card_pow_eq_one_le (Multiplicative α) _ _ (_) hn)
no goals
case mk.intro
α✝ : Type u
a : α✝
inst✝⁵ : Group α✝
inst✝⁴ : DecidableEq α✝
inst✝³ : Fintype α✝
hn✝ : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => n • a = 0) univ) ≤ n
g : Multiplicative α
hg : ∀ (x : Multiplicative α), x ∈ zpowers g
⊢ IsAddCyclic α
exact ⟨⟨g, hg⟩⟩