Structure theorem for finite(ly generated) abelian groups?

Stream: Is there code for X?

[Michael Stoll]

Is the statement that a finite / finitely generated abelian group is (isomorphic to) a product of cyclic groups somewhere in mathlib?
(Actually, I'm interested in the statement that when A is a finite abelian group, then the number of add_monoid_homs into the multiplicative group of a field is at most #A, but this is a consequence.)

[Kevin Buzzard]

The statement that a finitely generated module over a PID is a product of cyclic modules is currently in the process of being PR'ed.

[Oliver Nash]

cc @Pierre-Alexandre Bazin

[Riccardo Brasca]

The relevant PR is #13524

[Michael Stoll]

OK; so I'll wait a bit.

[Riccardo Brasca]

I am guilty of asking to develop the theory of right split exact sequences

[Michael Stoll]

I was thinking of adding a statement that any additive character on a finite ring R into a domain R' is a multiplicative shift of any given primitive additive character c. The idea being to show that the map from R to the set of characters that sends a to \lambda x, c (a*x) is injective, then to use the cardinality bound to get surjectivity.

[Michael Stoll]

But this is nothing I urgently need for what I am actually trying to do...

[Antoine Labelle]

Another possibility for proving that bound without the structure theorem is using the orthogonality of characters. I'm currently working on that for the general case of finite groups, and hopefully it shouldn't be too long before it gets into mathlib.