case mp
α : Type u
a : α
inst✝¹ : Fintype α
inst✝ : CommGroup α
⊢ IsSimpleGroup α → IsCyclic α ∧ Nat.Prime (Fintype.card α)

case mpr
α : Type u
a : α
inst✝¹ : Fintype α
inst✝ : CommGroup α
⊢ IsCyclic α ∧ Nat.Prime (Fintype.card α) → IsSimpleGroup α
α : Type u
a : α
inst✝¹ : Fintype α
inst✝ : CommGroup α
⊢ IsSimpleGroup α ↔ IsCyclic α ∧ Nat.Prime (Fintype.card α)
constructor
case mp
α : Type u
a : α
inst✝¹ : Fintype α
inst✝ : CommGroup α
h : IsSimpleGroup α
⊢ IsCyclic α ∧ Nat.Prime (Fintype.card α)
case mp
α : Type u
a : α
inst✝¹ : Fintype α
inst✝ : CommGroup α
⊢ IsSimpleGroup α → IsCyclic α ∧ Nat.Prime (Fintype.card α)
intro h
no goals
case mp
α : Type u
a : α
inst✝¹ : Fintype α
inst✝ : CommGroup α
h : IsSimpleGroup α
⊢ IsCyclic α ∧ Nat.Prime (Fintype.card α)
exact ⟨IsSimpleGroup.isCyclic, IsSimpleGroup.prime_card⟩
case mpr.intro
α : Type u
a : α
inst✝¹ : Fintype α
inst✝ : CommGroup α
left✝ : IsCyclic α
hp : Nat.Prime (Fintype.card α)
⊢ IsSimpleGroup α
case mpr
α : Type u
a : α
inst✝¹ : Fintype α
inst✝ : CommGroup α
⊢ IsCyclic α ∧ Nat.Prime (Fintype.card α) → IsSimpleGroup α
rintro ⟨_, hp⟩
case mpr.intro
α : Type u
a : α
inst✝¹ : Fintype α
inst✝ : CommGroup α
left✝ : IsCyclic α
hp : Nat.Prime (Fintype.card α)
this : Fact (Nat.Prime (Fintype.card α))
⊢ IsSimpleGroup α
case mpr.intro
α : Type u
a : α
inst✝¹ : Fintype α
inst✝ : CommGroup α
left✝ : IsCyclic α
hp : Nat.Prime (Fintype.card α)
⊢ IsSimpleGroup α
haveI : Fact (Fintype.card α).Prime := ⟨hp⟩
no goals
case mpr.intro
α : Type u
a : α
inst✝¹ : Fintype α
inst✝ : CommGroup α
left✝ : IsCyclic α
hp : Nat.Prime (Fintype.card α)
this : Fact (Nat.Prime (Fintype.card α))
⊢ IsSimpleGroup α
exact isSimpleGroup_of_prime_card rfl