∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (a : α),
  a ∈ NonUnitalSubsemiring.center α ↔
    AddMonoid.End.mulRight a = AddMonoid.End.mulLeft a ∧ AddMonoid.End.mulLeft a ∈ (CentroidHom.toEndRingHom α).rangeS