exists_nonabelian_leinster_group

Non-abelian Leinster groups exist. For example, `S₃ × C₅` (order 30) and `A₅ × C₁₅₁₂₈` are Leinster groups. Reference: Leinster, Tom (2001). "Perfect numbers and groups".

theorem exists_nonabelian_leinster_group :
    ∃ G : Type, ∃ (_ : Group G) (_ : Fintype G),
      IsLeinster G ∧ ¬ ∀ (a b : G), a * b = b * a

Recent Submissions

No submissions yet. Be the first to attempt this problem.