Isolating terms of a finite sum

Stream: Is there code for X?

[Vivek Rajesh Joshi]

I'm finding it a bit hard to locate this piece of code. If I have a finite sum over some f x, where x : Fin m, and I want to write the sum as f y + sum over all x that aren't y, how do I do it?

[Edward van de Meent]

docs#Finset.sum_insert might be of help

[Vivek Rajesh Joshi]

That's pretty close to what I want, the only problem is that this is a sum over a set Finset a and I'm dealing with a sum over a type Fin m. How do I reconcile the two?

[Ruben Van de Velde]

A sum over Fin m is actually a sum over Finset.univ : Finset (Fin m)

[Ruben Van de Velde]

Actually docs#Finset.add_sum_erase might be even better

[Yury G. Kudryashov]

@loogle Finest.univ, Fin.succAbove

[loogle]

:exclamation: unknown identifier 'Finest.univ'
Did you mean "Finest.univ", Fin.succAbove?

[Yury G. Kudryashov]

@loogle Finset.univ, Fin.succAbove

[loogle]

:search: Fin.image_succAbove_univ, Fin.univ_succAbove, and 12 more

[Yury G. Kudryashov]

@loogle Finset.univ, Fin.succAbove, Finest.sum

[loogle]

:exclamation: unknown identifier 'Finest.sum'
Did you mean Finset.univ, Fin.succAbove, "Finest.sum"?

[Yury G. Kudryashov]

@loogle Finset.univ, Fin.succAbove, Finset.sum

[loogle]

:search: Fin.sum_univ_succAbove, Matrix.det_succ_column_zero, and 9 more

[Yury G. Kudryashov]

New phone insists on correcting Finset to finest

[Daniel Weber]

There is docs#Finset.sum_eq_add_sum_diff_singleton