monoid.exponent_exists_iff_ne_zero source