Add an exercise on ring theory and the first isomorphism theorem

[Vierkantor]

A tour through the fundamental definitions of ring theory in Mathlib ending with a little proof of the first isomorphism theorem.

I noticed aesop is misconfigured in Mathlib: MulMemClass.mul_mem should not be marked [aesop safe] since there are other ways to prove the same goal. So we need to put some magic lines in the header:

attribute [-aesop] mul_mem add_mem
attribute [aesop unsafe apply (rule_sets := [SetLike])] mul_mem add_mem Ideal.mul_mem_left Ideal.mul_mem_right

I'll upstream this to Mathlib too.