Infinite residually finite group is not simple (source code)

= Infinite residually finite group is not simple

An infinite residually finite group is not a <simple group>. For a nonidentity element, residual finiteness supplies a map to a finite group in which it survives. Its kernel is proper and cannot be trivial, since an infinite group cannot inject into a finite group.