feat: add `Fin.sum`, `Fin.prod`, `Fin.count`

[fgdorais]

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch batteries-pr-testing-1460 has successfully built against this PR. (2025-10-12 07:43:05) View Log
• ✅ Mathlib branch batteries-pr-testing-1460 has successfully built against this PR. (2025-11-29 02:58:46) View Log

[linesthatinterlace]

Nice PR, but I do have some thoughts.

[fgdorais]

Those are reasonable and important thoughts. My preference here is to further develop the List versions in Batteries and basically just have the translation from Fin functions to List functions here. I opened issue #1465 for this.

The idea here is that the Fin functions only exist for efficiency: they do exactly the same as the List functions but they avoid the time and memory required for constructing the intermediate lists.

[linesthatinterlace]

I think that is reasonable. Though you might also want a theory for Vector n and that is even more analogous to this Fin case: I suspect in both Fin and Vector cases you will want theorems that are a thin layer onto List, but it's List where you should generally do the proofs (that is what it is for!)

[linesthatinterlace]

I think for me the key distinction between Fin and List is that that List privileges a :: l over l ++ [a], and quite rightly so, but Fin should not privilege (f 0, f (x.succ)) over (f (x.castSucc), f (last _).