[Merged by Bors] - refactor(data/finsupp/antidiagonal): Make antidiagonal a finset

[BoltonBailey]

Pursuant to discussion here

Refactoring so that finsupp.antidiagonal and multiset.antidiagonal are finsets.

Still TO DO: multiset.antidiagonal

---

[digama0]

Also mentioned on zulip, but I disagree with the refactor of multiset.antidiagonal. That function is written exactly the way it is intended to be. The antidiagonal function that I think Bolton wants could however be extracted into a typeclass on ordered monoids:

class has_antidiagonal (α : Type*) [ordered_add_comm_monoid α] :=
(antidiagonal : α → finset (α × α))
(mem_antidiagonal {{a b c : α}} : (a, b) ∈ antidiagonal c ↔ a + b = c)

This has instances for nat, multiset, finset, and α →₀ β where β has an antidiagonal function. Maybe it needs a different name to distinguish it from the existing function though.

[BoltonBailey]

I like @digama0 's suggestion of a has_antidiagonal class, but I am working on another project and don't have time to implement it right now. Can I ask that this PR be reviewed now and an issue be opened so that the has_antidiagonal class is still on the mathlib radar?

[fpvandoorn]

Can I ask that this PR be reviewed now

I think Mario's suggestion is to not remove the current version of finsupp.antidiagonal, but add a new class / definition that has the behavior you want. Your PR removes the current finsupp.antidiagonal.
I also think that the current definition of finsupp.antidiagonal (before this PR) is a natural one to have, but feel free (as Mario suggested) to rename it to finsupp.antidiagonal' and add finsupp.antidiagonal for its support (or define the above class has_antidiagonal).

[BoltonBailey]

I also think that the current definition of finsupp.antidiagonal (before this PR) is a natural one to have, but feel free (as Mario suggested) to rename it to finsupp.antidiagonal' and add finsupp.antidiagonal for its support (or define the above class has_antidiagonal).

Yes, thanks for reminding me of this. I have now restored the original definition as finsupp.antidiagonal'.

[BoltonBailey]

Created ticket for has_antidiagonal here

[fpvandoorn]

LGTM

[eric-wieser]

Suggested change

	simp [antidiagonal, ← and.assoc, ← finsupp.to_multiset.apply_eq_iff_eq]
	simp [antidiagonal, antidiagonal', ← and.assoc, ← finsupp.to_multiset.apply_eq_iff_eq]

[BoltonBailey]

This change needs to be made in two places, I have committed it, we'll see if it fixes it.

[fpvandoorn]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests