Commit 2026-01-08 08:52 4d0407b3

feat(GroupTheory/SpecificGroups/Cyclic): generalize the proof of prime_card by not assuming Finite (#32152) previously the proof of prime_card assumes Finite, which could derived from the premises of CommGroup and IsSimpleGroup. This PR adds a theorem of finiteness of commutative simple group, a theorem of prime_card which dosen't assume Finite, and a theorem of isomorphism from any commutative simple group to ZMod p, where p is a prime number.