Commit 2024-02-15 20:02 18b3970e

feat: Variant of structure theorem of finite abelian groups (#10587) where the trivial factors have been dropped. I have the idea of a general approach to dropping trivial terms from a direct sum. However it is too complicated for me to unsorry it and overkill here, so I am leaving it as a comment. From LeanAPAP