Commit 2025-04-03 15:49 727d0ff3

chore(GroupTheory/FreeAbelianGroupFinsupp): split file (#23626) There are two very distinct things going on in this file:

1. The free abelian group with generators α is isomorphic to finitely supported function α →₀ ℤ.
2. Isomorphisms of free abelian groups come from equivalences of their generators. 2 depends on 1, but also on a huge lot of linear algebra (it needs the invariant basis number theorem). Therefore, splitting the file along 1 and 2 makes 1 much lighter. This is what this PR does.