mathlib

07fb3d7e - refactor(data/finsupp/antidiagonal): Make antidiagonal a finset (#7595)

refactor(data/finsupp/antidiagonal): Make antidiagonal a finset (#7595) Pursuant to discussion [here](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/antidiagonals.20having.20multiplicity) Refactoring so that `finsupp.antidiagonal` and `multiset.antidiagonal` are finsets. ~~Still TO DO: `multiset.antidiagonal`~~