PR for GroupTheory/SpecificGroups/Cyclic

Stream: mathlib4

[Lingyin Luo]

Hello everyone :)

My name is Lingyin. I am a bachelor student learning Lean and abstract algebra. I am currently doing a project which formalizing some basic group theories by using mathlib.

While formalizing the isomorphism theorem between any abelian simple group and ZMod p(where p is a prime number), I noticed that the existing lemma in mathlib assumes finiteness, though finiteness could actually be derived from the premises.

So I added a a proof of finiteness of abelian simple group, placed it in GroupTheory/SpecificGroups/Cyclic, and modified the related theorems accordingly.

My PR is here: #32152. I would be very grateful if anyone had time to have a look at this PR and give suggestions, thanks a lot!