Group_is_not_Empty
Provedgroup-theoryproofwiki
A group cannot be empty, as it must contain at least the identity element.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Group_is_not_Empty {G : Type _} [Group G] : Nonempty G := by sorrySource