Monoid_is_not_Empty
Provedmonoidsproofwiki
A monoid cannot be empty, as it must contain at least the identity element.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Monoid_is_not_Empty {M : Type _} [Monoid M] : Nonempty M := by sorrySource